On 31/05/2012 01:27 PM, scott wrote:
>>> Runs fine here, opened it up and was thinking what it could be useful
>>> for ... could it be used to solve Sudoku puzzles?
>>
>> It... could. Perhaps. With some serious modifications.
>
> You would need a permutation predicate, eg LPerm. It would be solved
> when the first list is a permutation of the second list.

Challenge accepted. ;-)

Actually, there is /already/ an SEqual{} predicate, which is solved if 
two lists are "set-equal". That is, X is a subset of Y and Y is a subset 
of X. More simply, every element of X is also an element of Y and vice 
versa.

Notice that this does not imply that X is a /permutation/ of Y, since 
elements can appear more than once. (Remember, sets do not have 
multiplicity.) If I could fix that, it might work.

> LPerm{ List[1,2,3] , List[3,1,x] }
>
> Would tell you that x := 2

That doesn't quite work for SEqual{}, because every set can be 
represented by infinity distinct lists. But it ought to be fixable.

> I'm guessing that it wouldn't be simple to implement...

I'm guessing that it would. ;-)

The trick appears to be either to get the loop to terminate reliably, or 
else to somehow add a constraint that both lists are the same size.

> If you had that, then you could expand it easily to a sudoku grid. You'd
> need an LPerm for each row, each column and each 3x3 box all ANDed
> together.
>
> Now that would be a very cool solution, as in you wouldn't need to tell
> the computer *how* to solve it (as you have to when writing a
> "traditional" sudoku solver), just what the rules are.

I'll see what I can come up with...

Post a reply to this message

On 31/05/2012 02:32 PM, Invisible wrote:

> Actually, there is /already/ an SEqual{} predicate, which is solved if
> two lists are "set-equal". That is, X is a subset of Y and Y is a subset
> of X. More simply, every element of X is also an element of Y and vice
> versa.

Ha! Yes, SEqual{} is already defined. It also doesn't /work/. o_O

The mistake is simple. SEqual{} calls SSubset{}, and SSubset{} has a 
bug. Its definition is

SSubset{sub, super}:
   (sub = End[]) | (~item ((SMember{item, sub}) & (SMember{item, super})))
;

In other words,

   "S is a subset of T if S is the empty set OR _there exists_ an X 
which is a member of S and a member of T."

What it /should/ of course say is

   "S is a subset of T if S is the empty set OR _for all_ X which is a 
member of S, X is a member of T."

In short, I've mixed up "exists" and "for all". Kind of an important 
distinction, that one.

Logic Box of course doesn't /have/ an explicit for-all construct. At 
this point I am uncertain whether I can work around that...

Post a reply to this message

On 31/05/2012 02:57 PM, Invisible wrote:

> Ha! Yes, SEqual{} is already defined. It also doesn't /work/. o_O
>
> The mistake is simple. SEqual{} calls SSubset{}, and SSubset{} has a
> bug.

> In short, I've mixed up "exists" and "for all". Kind of an important
> distinction, that one.
>
> Logic Box of course doesn't /have/ an explicit for-all construct. At
> this point I am uncertain whether I can work around that...

A /correct/ definition for SSubset{} is

SSubset{subset, superset}:
   (subset = End[]) |
   (~head ~tail
     subset = Node[head, tail] &
     SMember{head, superset} &
     SSubset{tail, superset}
   )
;

Before SSubset{} would accept any pair of sets where just one element is 
common to both sets. Now it only works if /all/ of the elements of the 
subset are elements of the superset. (I.e., it works correctly now.)

This in turn causes SEqual{} to function correctly.

It's quite slow, but

   SEqual{List[1, 2, 3], List[3, 1, x]}

does eventually yield x := 2.

QED.

Post a reply to this message

On 31/05/2012 2:26 PM, Invisible wrote:
> Well, right now - oh, wait, legally I can't tell you about that. Maybe
> in a few weeks' time...

I am all agog.

-- 
Regards
     Stephen

Post a reply to this message

> This in turn causes SEqual{} to function correctly.
>
> It's quite slow, but
>
> SEqual{List[1, 2, 3], List[3, 1, x]}
>
> does eventually yield x := 2.

So for the first row in a sudoku I'd expect something like this:

SEqual{List[1..9], List[3,a,b,c,1,d,e,f,8]}

That should work, as both lists are the same length (so the 2nd list 
must contain the each of the elements 1-9 once).

But I'm guessing it's going to be very slow, especially when you add in 
the other 26 SEqual statements all ANDed together...

Shame, as I think it's a really neat way to write a solver.

Post a reply to this message

On 31/05/2012 03:56 PM, scott wrote:
>> This in turn causes SEqual{} to function correctly.
>>
>> It's quite slow, but
>>
>> SEqual{List[1, 2, 3], List[3, 1, x]}
>>
>> does eventually yield x := 2.
>
> So for the first row in a sudoku I'd expect something like this:
>
> SEqual{List[1..9], List[3,a,b,c,1,d,e,f,8]}
>
> That should work, as both lists are the same length (so the 2nd list
> must contain the each of the elements 1-9 once).
>
> But I'm guessing it's going to be very slow, especially when you add in
> the other 26 SEqual statements all ANDed together...
>
> Shame, as I think it's a really neat way to write a solver.

When I removed the run time constraint, it took Logic Box about 22 
seconds and 90 MB of RAM to come up with the first 10 solutions to the 
predicate above. Of course, it's going to sit there and search for all 
6! permutations of 6 items.

Think about what's happening under the covers: Logic Box is merely 
searching through all possible combinations, trying to find one for 
which all the constraints apply. I should imagine that for Sudoku, the 
search space is /astronomical/, so it's likely to take a while. If it 
takes 22 seconds to partially process one row, then processing 9 rows, 9 
columns and 9 squares searching for a simultaneous solution to all of 
them is going to take... a while.

I agree, however, that it would be very cool if this actually worked. :-D

Post a reply to this message

scott <sco### [at] scottcom> wrote:
> Also how hard would it be to add support for arithmetic operators?

yes, first thing I tried was changing x=y to x=2*y

hmm, didn't actually tried x=2y...

> Having written something like this is also very good for CVs and job
> interviews :-)

yes, at least if he's willing to change "written by Orphi the AweKid"... :p

On AI, perhaps we don't have bad and mean counscious AI, but OTOH, we have far
more believable game characters than we've ever dreamed for back then... IBM
also got Watson... a few more years and we may get Sherlock level... :)

Post a reply to this message

Attached is release #2.

Only a few things have changed. The laughable bug in SSubset{} is gone, 
and the file requester doesn't keep resetting itself to your home folder 
every single time you open it. I've also adjusted it so that temporary 
variables are labelled with their original names as subscripts, which 
makes things slightly easier to follow. (But only slightly.)

There's a couple of other ideas I have for what could be done with this 
program. (E.g., improving the output, refactoring the code, adding new 
features.) But honestly, I think I'm bored with it now. I don't suppose 
I'll be making any further releases soon. It's time for a different 
project...

Post a reply to this message

Attachments:
Download 'logicbox-02 release2.jar.zip' (197 KB)

Theorem: The language implemented by Logic Box is Turing-complete.

Proof: I have written a program in Logic Box which executes any program 
written in the SKI calculus. The SKI calculus is known to be 
Turing-complete.



Actually, things are not quite so simple. But here goes...

First, the SKI calculus consists of abstract variables, and the three 
combinators "S", "K" and "I", which have the following rules:

   Sfgx => (fx)(gx) => fx(gx)
   Kxy  => x
   Ix   => x

It may seem absurd that this trivial system is Turing-complete. But 
there is actually several even /more/ trivial systems which are somehow 
Turing-complete.

So, how do we implement these transformation rules in Logic Box? Well, 
first we need to decide how to store this stuff. I have chosen to use 
S[], K[] and I[] to stand for the three combinators, and used the 
structure at[x, y] to represent a function application. (In other words, 
what is normally written as "xy" becomes "at[x, y]".) This makes things 
very verbose, but it does work.

The actual transformation rules are now simple enough to write:

   Reduce1{in, out}:
     (~x in = at[I[], x] & out = x) |
     (~x y in = at[at[K[], x], y] & out = x) |
     (~f ~g ~x in = at[at[at[S[], f], g], x] & out = at[at[f, x], at[g, x]])

This simple predicate takes an SKI expression as its first argument, and 
arranges for the second argument to be made equal to the result of a 
single reduction.

Actually, to get a "complete" reduction, you need to add a few extra 
rules to recursively reduce sub-expressions, or the thing never makes 
any progress.

This only performs one reduction step. To make it reduce /all/ the 
steps, you can do

   Reduce{in, out}:
     out = in | ~new Reduce1{in, new} & Reduce{new, out}

Unfortunately, because the OR operator tries /all/ possibilities rather 
than just keeping the first successful one, what this does is to produce 
a result set containing all possible reductions, using all possible 
reduction orders.

So in summary, we can say that running the program produces a result set 
which contains the correct answer /somewhere/, plus a whole heap of 
various intermediate results. As best as I can tell, there's no way to 
determine /where/ in the solutions it is. So I'm not completely sure 
this counts as a valid proof.

The complete test code is here:

Reduce1{in, out}:
   (~arg1 at[I[], arg1] = in & out = arg1) |
   (~arg1 ~arg2 at[at[K[], arg1], arg2] = in & out = arg1) |
   (~fn1 ~fn2 ~arg3 at[at[at[S[], fn1], fn2], arg3] = in & out = 
at[at[fn1, arg3], at[fn2, arg3]]) |
   (~left ~right
     at[left, right] = in &
     (
       ( ~left2 Reduce1{ left,  left2} & out = at[left2, right ]) |
       (~right2 Reduce1{right, right2} & out = at[left , right2])
     )
   )
;

Reduce{in, out}:
   in = out | ~new Reduce1{in, new} & Reduce{new, out}
;

Test1{out}:
   ~s s = S[] &
   ~k k = K[] &
   ~i i = I[] &
   out = at[at[at[at[s, at[at[s, at[k, s]], k]], i], f[]], x[]]
;

The final bit generates the expression S(S(KS)K)Ifx - the Church numeral 
2 - as a simple example which you can run.

   Test1{test} & Reduce{test, out}

It takes many, many steps, but it does eventually produce f(fx) as 
result #7. (And several more times after that, as it explores every 
possible reduction sequence. The number of these is presumably 
exponential in the size of the input...)

I would have to add either a NOT predicate, or an exclusive-OR predicate 
to get this to terminate at normal form.

Post a reply to this message

On 01/06/2012 11:48 AM, Invisible wrote:

> It takes many, many steps, but it does eventually produce f(fx) as
> result #7. (And several more times after that, as it explores every
> possible reduction sequence. The number of these is presumably
> exponential in the size of the input...)

Not so much the /size/ of the input, but the number of redexes 
("reducible expressions") it contains.

At every point, the solver chooses a redex by some algorithm, and then 
reduces it. Overall, the solver makes all possible choices, and 
generates [at least] one result per choice. So clearly the number of 
redexes put a lower bound on the number of solutions.

Reducing a K-redex or an I-redex results in one fewer redexes. However, 
reducing an S-redex can duplicate an existing redex into /two/ new 
redexes. (Or it can leave the number of redexes unchanged. It depends on 
the exact expression.)

I would hazard a guess, therefore, that the number of possible reduction 
orders is a non-computable function of the input expression.

Look at it this way: It appears that the only way to compute the number 
of reduction orders is to actually /find/ all possible reduction orders. 
In other words, to execute the program and count how many ways you can 
do it. If the program is non-terminating, then the counting procedure is 
also non-terminating. So it appears that counting the number of 
reduction orders is trivially equivalent to the Halting Problem.

(This relies on the assumption that running the program is the /only/ 
way to compute the number of reduction orders...)

Post a reply to this message