I haven't attempted to actually compile and run any Java code for about 
10 years now. So for the past month, I've been writing Java code. I will 
probably write about the actual coding experience later; right now I 
want to talk about what I've produced.

It's a small program called Logic Box. It lets you do logic programming, 
after a fashion.

More exactly, Logic Box solves predicates. For the purposes of this 
discussion, a "predicate" is simply a logical statement which may be 
true or false. For example, 2 = 2 is obviously true, while 5 = 7 is 
clearly false.

Given such a statement, Logic Box can tell whether it is true or false. 
But that's pretty easy, really. The interesting part is that a predicate 
may contain /variables/. Such a predicate is now no longer simple "true" 
or "false"; it depends on what the variables contain. So we can write 
predicates which are /sometimes/ true and /sometimes/ false.

Given such a predicate, Logic Box will attempt to /make/ the predicate 
true. That is, it tries to figure out what you need to set the variables 
to in order to "solve" the predicate (i.e., make it true).

The simplest kind of predicate is the equal predicate. It compares two 
expressions (not predicates) and is satisfied if both expressions are 
/identical/, once any bound variables have been replaced with the values 
they are bound to. Not all variables have to be bound to something; for 
example, x = x is unconditionally true, regardless of what value x has.

There are currently three sorts of expression: an integer, a variable 
name, or a "record". A record has a name and zero or more fields, which 
are arbitrary expressions. (In other words, records can be nested to any 
depth.) You can use the name of the record as the actual data. For 
example, Foo[] and Bar[] are two distinct values. Or you can use the 
name to indicate the "sort" of data, and the fields to represent the 
actual data. For example, Date[28, 03, 1980] or Time[09, 27, 56]. (Both 
of these are three integers, but they are not comparable because the 
names are different.)

(Note carefully: "Foo" is a variable, "Foo[]" is a record.)

Solving a predicate such as 7 = x isn't hard. The solution is simply x 
:= 7. (Logic Box uses the notation that "=" denotes a /test for/ 
equality between two arbitrary expressions, while ":=" denotes the 
/assignment/ of a value to a variable, otherwise known as a "binding".) 
But consider the predicate

   Triple[a, x, y] = Triple[1, Pair[2, a], Pair[x, 7]]

Can this be solved? Actually yes, it can:

   a := 1; x := Pair[2, 1]; y := Pair[Pair[2, 1], 7]

If you take the original predicate and replace each variable with the 
corresponding binding, you will find that

   Triple[1, Pair[2, 1], Pair[Pair[2, 1], 7] = Triple[1, Pair[2, 1], 
Pair[Pair[2, 1], 7]

Clearly both sides are identical, so the predicate is solved.

Notice how variables are not limited to containing integers; they may 
contain arbitrary expressions - even expressions involving other 
variables. However, a variable can never be bound to an expression 
containing itself. That would result in an infinite loop. So something 
like x := Pair[1, x] is not allowed. (Imagine trying to replace every x 
with Pair[1, x]. The process never halts.)

As well as the equal predicate, you can use the usual AND ("&") and OR 
("|") operators. By default, the operator precedence is =, &, |, in that 
order. You can use brackets to override this as usual. (There is a 
slight glitch: brackets are not allowed inside expressions, only inside 
predicates. So "Pair[(x), (y)] = z" is not allowed, neither is "(Pair[x, 
y]) = z", but "(Pair[x, y] = z)" is fine.)

The meaning of AND is pretty obvious; the predicate is solved only if 
the solution solves /both/ child predicates simultaneously. The meaning 
of OR is equally obvious. What is perhaps /not/ obvious is that 
predicates involving OR can have /multiple solutions/. Consider, for 
example, x = 1 | x = 2. This has two solutions, x := 1 and x := 2. In 
general, a given predicate can have an unlimited number of solutions, 
and Logic Box will attempt to find all of them for you.

Perhaps most interestingly of all, you can define "named predicates", 
which behave something like subroutines. In particular, a named 
predicate can invoke itself recursively, creating a way to implement 
loops. (This would otherwise be impossible.)

Logic Box comes with a small bunch of named predicates, mostly to do 
with list processing. All the list predicates begin with "L". Some 
predicates take a list, but treat it as a poor man's set. These begin 
with "S".

As an example, the SMember{} predicate tests whether a given item is a 
member of a set (actually a list). So, for example,

   SMember{2, List[1, 2, 3]}

is true, while

   SMember{5, List[1, 2, 3]}

is false.

Perhaps the most fascinating thing about logic programming is that you 
can write a predicate like SMember{}, and once written, it works 
forwards /and backwards/! For example,

   SMember{5, List[1, x, 3]}

has one solution, namely x := 5. Logic Box doesn't tell you /if/ the 
predicate is true; it tells you how to /make/ it true. In this case, by 
inserting the 5 into the set. We haven't told Logic Box to do this; the 
code for SMember{} doesn't say how to accomplish such a thing. It's just 
an automatic consequence of the language.

We could similarly have written

   SMember{5, List[x, y, z]}

This generates 3 solutions:

   x := 5;
   y := 5;
   z := 5;

Clearly each of these solves the predicate. Alternatively,

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

has solutions

   x := 1;
   y := 2;
   z := 3;

Here what we have done, in effect, is to make Logic Box loop over all 
the elements of the set. So SMember{} can mean "/is/ this a member of 
the set?", but it can also mean "/get/ a member of the set". You could 
them write a second predicate involving x, join them with an AND, and 
Logic Box will find any solutions there might be. For example,

   SMember{x, List[1, 2, 3]} & SMember{x, List[2, 4, 6, 8]}

will find any elements in the intersection of the two sets. (In this 
case, x := 2 is the only solution.) Replace the AND with an OR and you 
get the union of the sets instead.

Another, more list-oriented predicate is LJoin{}. This works in a 
slightly strange way. Given three lists, the predicate is satisfied if 
joining the first two lists together yields the last list. For example,

   LJoin{List[1, 2, 3], List[4, 5, 6], List[1, 2, 3, 4, 5, 6]}

is true, because List[1, 2, 3] + List[4, 5, 6] = List[1, 2, 3, 4, 5, 6].

In this form, the predicate is testing /if/ joining two lists yields a 
third. But if we replace the third list with a variable name, Logic Box 
will /make/ the predicate true, by computing what the join of the two 
lists is:

   LJoin{List[1, 2, 3], List[4, 5, 6], out}

   out := List[1, 2, 3, 4, 5, 6]

So we can test /if/ this is the join of two lists, or we can /get/ the 
join of two lists. But we can also run this backwards:

   LJoin{List[1, 2, 3], y, List[1, 2, 3, 4, 5, 6}

   y := List[4, 5, 6]

Logic Box has stripped the prefix 1, 2, 3 off of our long list. We 
didn't tell it how to do that in the code for LJoin{}; again, it's 
automatic. We can /even/ to this:

   LJoin{x, y, List[1, 2, 3, 4, 5, 6]}

This has 7 solutions:

   x := List[]; y := List[1, 2, 3, 4, 5, 6];
   x := List[1]; y := List[2, 3, 4, 5, 6];
   x := List[1, 2]; y := List[3, 4, 5, 6];
   x := List[1, 2, 3]; y := List[4, 5, 6];
   x := List[1, 2, 3, 4]; y := List[5, 6];
   x := List[1, 2, 3, 4, 5]; y := List[6];
   x := List[1, 2, 3, 4, 5, 6]; y := List[];

Again, Logic Box has performed a search and discovered every possible 
way of satisfying the predicate - in other words, every possible way to 
split a list in half. So the /joining/ predicate can be used for 
/splitting/.

We can of course go still further, doing loopy things like

   LJoin{List[x, y, z], w, List[1, 2, 3, 4, 5, 6]}

to fetch the first three elements of the list plus the remainder. You 
could of course implement all of this functionality in a normal 
programming language; logic programming just lets you do it all with one 
small piece of code.

Beware that it's very easy to ask a question which has infinity answers. 
For example,

   LJoin{x, y, z}

has infinity solutions, as Logic Box attempts to construct all possible 
lists of every combination of sizes. Also, sometimes a predicate 
/doesn't/ work in a particular direction; for example LReverse{} works 
forwards, but goes into an infinite search if run backwards. It depends 
on the exact order in which Logic Box searches the solution space, which 
depends on the exact way in which the predicate is phrased.

I should point out that the examples above don't actually work as 
written. I describe expressions such as List[1, 2, 3] as "packed lists". 
The language provides no way to iterate over such structures. Instead, 
you have to use "unpacked lists", which look like

   Node[1, Node[2, Node[3, End[]]]]

Clearly that's much more typing (although it allows easy iteration). 
There's an LUnpack{} predicate which can unpack a list for you. (It uses 
an internal hard-wired language primitive to achieve this feat.) There 
ought to be one LPack{} predicate, but unfortunately we need a separate 
LPack{} and LUnpack{}, due to issues to search space ordering. (The two 
predicates have identical implementations, except for the ordering of 
their terms.)

[In future, I might make LPack{} itself a hard-wired primitive, allowing 
it to work in any direction. It's mildly annoying that this is necessary 
though...]

As an example of use,

   LUnpack{List[1, 2, 3], x} & LReverse{x, y} & LPack{out, y}

In both LPack{} and LUnpack{}, the first argument is a packed list, and 
the second is an unpacked list. The difference is which one is the 
"input" and which the "output". (Alternatively, you can just write out 
the unpacked lists by hand. It's not /that/ hard to do...)

Now that we know about unpacked lists, let's look at the source code for 
LJoin{}:

   LJoin{xs, ys, zs}:
     (xs = End[] & ys = zs) |
     (~head ~tailX ~tailZ
       xs = Node[head, tailX] &
       zs = Node[head, tailZ] &
       LJoin{tailX, ys, tailZ}
     )
   ;

That's /it/. That's the whole thing. That's how we can join, strip and 
split lists all at once. That's all there is to it.

So how does it work? Well, the first line says that the predicate can be 
satisfied if the first list is empty, and the second two lists are 
identical. (I.e., prefixing nothing does nothing.)

The notation "~x ..." means "there exists a value x such that ..." 
Essentially what it does is to create a local variable. As you can see, 
LJoin{} calls itself recursively, so we don't want variables from 
different invocations clashing because they have the same name. (The 
arguments to a predicate are automatically local, by a different mechanism.)

So, the equations are saying:

1. Both xs and zs are Node[] (not End[]).
2. There exists a value (head) which is the first element of xs and zs.
3. Recursively, join the tails of the lists.

Eventually we will reach the end of xs, terminating the loop. We see 
that either xs = End[] or xs = Node[]. These two possibilities are 
mutually exclusive; they cannot both occur. So - provided xs is defined 
- eventually the loop must end.

What might /not/ be clear is how this generates multiple solutions in 
cases such as LJoin{x, y, List[1, 2, 3]}. Where is the "searching" 
happening? Well, that would be the OR operator. It tries both 
alternatives. Look again at the solutions list: the /first/ solution is 
xs = End[] and ys = zs, because that's the first line in LJoin{}.

Next, it tries xs with one element. It knows what element, because zs = 
Node[head, tailZ], and zs is defined to begin with a 1, so xs must begin 
with a 1. In this fashion, it can iterate over all the possible splits. 
Eventually we reach the point where zs = End[] rather than Node[], so 
the second case fails, and only the first case is applicable, ending the 
loop.

You may find it entertaining to try to write some more predicates of 
your own - e.g., to add a new element to a set-list if not already 
present, to interleave to lists, etc.



So that's what Logic Box /does/. But how does it /work/?

Well, implementing Logic Box is about 50 lines of Haskell. It's a bit 
more in Java, but it's not /that/ big. I spent about 90% of my 
programming effort on making Logic Box /interactive/. It actually 
/shows/ you what it's doing, as it does it.

(Unfortunately, for mildly complicated predicates, the result just ends 
up being a giant wall of text which is still disappointingly hard to 
follow. But I tried...)

So, let's start with the equal predicate. This compares two expressions. 
If there are no variables involved, you simply compare the two 
expressions, and either they are already identical, or they will never 
be identical. So that's easy. But what if there are variables?

The general algorithm is apparently called "unification". It's 
surprisingly simple, although it is quite fiddly to get right.

The general idea is to compare the two expressions. If they are 
identical, you're done. If one of the expressions is a variable, you 
bind it to the other expression. (I.e., you make the other expression 
the variable's value.) But what if the variable /already/ has a binding? 
Well, you /could/ try unifying the new value against the existing one, 
but that gets kinda messy. There's a much simpler way.

What you do is you "cook" the expressions before unifying them. That is, 
you replace any variables which already have bindings with the 
expressions they're bound to. In this way, any variables which already 
have bindings vanish from the input, and by unifying the inputs you're 
automatically unifying the contents of those variables. It's much easier 
to program that way.

There is one slight bit of trickiness. Consider the predicate

   x = y & y = 5

Logic Box answers that the solution is

   x := 5; y := 5;

which is true. However, when unifying the first equality, we get the 
partial solution x := y. When we unify the second one, we add y := 5. So 
at this point, we have

   x := y; y := 5;

To get from this to the final result, we perform a "simplification". 
This basically involves looking up every variable and cooking its 
expression using the current solution. If the expression changes in this 
process, set the cooked expression as the variable's new expression and 
restart the loop. The loop terminates when no amount of cooking changes 
any expression.

So, the complete algorithm is this:

1. Cook both expressions.

2. If both expressions are identical, success.

3. If one of the expressions is a variable:
   A. If the variable appears in the other side as well, fail.
   B. Bind the variable to the other expression.
   C. Run the simplification loop.
   D. Success.

4. If both expressions are records:
   A. If the record names do not match, fail.
   B. If the field counts do not match, fail
   C. Unify each pair of fields in turn.

So unification works with a "current solution", which is gradually 
extended as more data is processed. In particular, the final step above 
performs unification recursively. The outer unification fails if any of 
the inner ones fail. Otherwise, the updated output from each sub-step 
feeds into the next sub-step, until no more steps remain.

The AND predicate is very simple on paper, but was the hardest one to 
program. In theory, you run each predicate until it produces a result, 
and then run the next predicate with the result from the previous step 
as its initial solution.

Oh, wait, predicates can potentially produce /multiple/ solutions, remember?

This means that you have to try all possible combinations. Again, on 
paper, that's simple:

   out1 := run predicate 1 [initial solution]
   for each solution1 in out1
     out2 := run predicate 2 [solution1]
     for each solution2 in out2
       out3 := run predicate 3 [solution2]
       for each solution3 in out3
         ...

Doing it interactively is damned fiddly. You have to be able to stop and 
restart multiple nested loops. It took me a while to figure that out. 
The algorithm I ultimately came up with is this:

1. Set the current predicate to predicate 1.

2. Run the current predicate.

3. If a solution is received:
   A. If this is the last predicate, return the solution.
   B. Pass the solution to the next predicate, and make that the current 
one.

4. If EOF is received:
   A. If this is the first predicate, return EOF.
   B. Make the previous predicate the current one.

As far as I can tell, this algorithm works. But it took a heck of a lot 
of trial and error to get to this point.

By contrast, the OR predicate is very easy. Just run each predicate in 
turn until EOF is received. Note that unlike AND, with OR every 
predicate gets an identical initial solution. (The initial solution for 
OR itself.) So the rules are simple; run current predicate, pass on any 
solutions received, move to the next predicate on EOF, end when you run 
out of predicates.

The way the "exists" predicate is implemented is slightly odd. This 
predicate consists of a variable name followed by a predicate. Each time 
it's run, it generates a unique ID number, and then replaces all 
occurrences of the local variable with this ID number. The resulting 
"cooked" predicate is then run as usual.

These unique IDs are called "temporary variables" (because usually they 
don't form part of the final solution, only the temporary internal 
state). They print out as ?1?, ?2?, ?3?, etc. (You can't type them in; 
they can only be created by exists.) You may from time to time see these 
pop up in a solution. Well, now you know what they are.

Named predicate calls are also very simple. You take the predicate name, 
look it up in a dictionary, check it's got the right number of 
arguments, replace each argument variable with the supplied argument 
value, and run the resulting predicate. Done.

As I mentioned, there's also a small number of named predicates who's 
implementation is actually hard-wired into the program. (I.e., it runs 
Java code rather than Logic Box code.) In particular, there's 
PRIM_True{} and PRIM_False{}, which unconditionally succeed or fail.

Post a reply to this message

On 31/05/2012 11:00 AM, Invisible wrote:
> Right now I want to talk about what I've produced.
>
> It's a small program called Logic Box. It lets you do logic programming,
> after a fashion.

Attached to this message is version 2, release #1 of Logic Box.

It's a single JAR file. If you double-click it, the program should fire 
up. You'll probably need Java 6 or newer.

(I developed it with NetBeans and JDK 6. It works fine on my Windows 
box, but I can't guarantee it will work elsewhere. You know how it goes; 
Write Once, Test Everywhere(tm)...)

As I explained at length in my previous message, Logic Box is a 
predicate solver. If you type a predicate into the top pane and jab 
"solve", Logic Box will attempt to solve it.

If the predicate is unconditionally true (e.g., 2 = 2), you will get one 
empty solution. If the predicate is unconditionally false (e.g., 7 = 5), 
you will get zero solutions. But predicates can have any number of 
solutions, and Logic Box will try to find them all.

By default, Logic Box tries to find 10 solutions, and then stops. Jab 
"more" to ask for the next 10. As a safety feature, Logic Box stops 
searching after 1,000 processing steps. (This is mainly so that if you 
write a dud predicate, you don't hang the whole program.) Again, jab 
more to let it run for another 1,000 steps; occasionally a valid 
predicate takes that long.

(Note: The Results pane always shows you the predicate that the 
solutions were generated from, in case you edited the predicate text and 
can't remember if you pressed Solve yet. The More button always 
generates more solutions for the predicate shown in the Results pane, 
not the one in the Input pane.)

The main feature of Logic Box, however, is that it shows you what the 
solver is actually /doing/ when it tries to solve a predicate. I'm not 
completely happy with the output, but it works after a fashion.

Pressing "solve" just prints out the solution(s), if any exist. To do an 
interactive session, click "interactive". You should see the Results 
pane go blank, and the State pane fill up with a description of the 
top-level predicate. (The Results pane will say "0 solutions"; that's 
just how many solutions have been found /so far/.) You can now jab Step 
to walk through the solution process. I won't attempt to describe it in 
detail; hopefully everything is moderately self-explanatory.

For example, the default predicate [which appears when you start the 
program] is "x = 1 & y = 2 | x = y & y = 5". Remember AND before OR, so 
that parses as ((x = 1) & (y = 2)) | ((x = y) & (y = 5)). The top-most 
predicate, then, is OR. So you get something like

   OR:
     Predicate #1: (x = 1) & (y = 2)
     Predicate #2: (x = y) & (y = 5)

When you jab Step, predicate #1 starts running. The top-most predicate 
here is AND, so we get something like

   AND:
     Predicate #1: x = 1
     Predicate #2: y = 2

These are both "equal" predicates, so we begin with

   Equal:
     Raw LHS: x
     Raw RHS: 1
     Cooked LHS: x
     Cooked RHS: 1

By settings x := 1, the cooked LHS changes from x to 1, which then 
matches the cooked RHS, solving the predicate. y = 2 is dealt with 
similarly, yielding solution #1. (You can watch it bubble up through the 
chain of predicates.)

The second branch is more interesting. Because OR is at the top, we 
start again with an empty set of bindings (rather than keeping the ones 
from the previous solution). The first predicate is x = y, which yields 
x := y. Then the second predicate is y := 5. This gives us

   x := y; y := 5;

You can then see a simplification step where the x := y is updated to x 
:= 5 (because y := 5). This gives us solution #2.

The process is a bit slower than it could be, because "equal" always 
generates exactly one solution, but AND and OR still have to test for 
the possibility of multiple solutions.

If you press the "library manager" button, you can see a list of all the 
named predicates currently defined. (LJoin{}, SMember{}, etc.) You can 
add new predicates by typing one into the lower pane and clicking Add. 
You can also click on an existing predicate to see its source code, or 
to remove it with the Delete button. You can even rename an existing 
predicate: Select it, edit the name in the text pane, Add it, and then 
Delete the old one.

There are a few predicates which are hard-wired. You can delete them, 
but you can never get them back again. (They're not definable from the GUI.)

You can hit Reset to reload the default library. There's also Load and 
Save buttons so you can keep your own favourite predicates on disk. It's 
just a standard text file, so you can write it using your favourite text 
editor rather than the crappy Java Swing text field if you wish. The 
parser is a little fragile though. Also, there is no syntax for 
inserting comments! (Note that loading and then saving a file /will/ 
mangle any brackets or white-space you might have added for clarity.)

OK, well, I think that's just about it... As I say, it's taken me about 
a month to write this. (In the good old "iterative prototype" model of a 
software life-cycle.) I'd like to say "I hope you like it", but I doubt 
anybody will actually play with it for more than 15 seconds...

Post a reply to this message

Attachments:
Download 'logicbox-02 release1.jar.zip' (196 KB)

>> Right now I want to talk about what I've produced.
>>
>> It's a small program called Logic Box. It lets you do logic programming,
>> after a fashion.
>
> Attached to this message is version 2, release #1 of Logic Box.

I think I remember reading your original post when you first wrote this 
in Haskell, a lot of it sounded very familiar...

Runs fine here, opened it up and was thinking what it could be useful 
for ... could it be used to solve Sudoku puzzles?

Also how hard would it be to add support for arithmetic operators?  Then 
you would have an equation solver, which arguably would be more useful.

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

Post a reply to this message

>> Attached to this message is version 2, release #1 of Logic Box.
>
> I think I remember reading your original post when you first wrote this
> in Haskell, a lot of it sounded very familiar...

Yep. It's from a chapter in the book "The Fun of Programming". (It's 
about FUNctional programming, see? See what they did there? >yawn<)

> 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.

Of course, /the/ canonical logic programming language is Prolog. 
Apparently when people first saw that thing back in the 1970s, everybody 
suddenly thought that human-level AI was just around the corner.

Logic Box doesn't have quite the same capabilities as Prolog. But the 
general idea is that you give Prolog "facts". You can then write 
"queries", and it uses logical deduction to solve them (much like Logic 
Box performs logical deduction).

For example, you might program in a family tree, and then ask queries 
like "Who is the most common ancestor of Jim and Fred?" or "Is Sam 
related to Jack?" Just like Logic Box, you don't actually /tell/ Prolog 
how to answer the question, you only tell it what it means for two 
people to be "related", and who is immediately related to who. The 
Prolog deduction system can them work out everything else from that. 
[Eventually...]

I gather people use this for things like diagnostic systems. You program 
in all the medical conditions and what their symptoms are. A doctor can 
then query the system with the symptoms presented, the system can decide 
which tests could be most diagnostic in eliminating similar illnesses, etc.

Watching Prolog at work, it's almost /frightening/ how much stuff it can 
figure out by itself, seemingly by magic. Indeed, before I wrote Logic 
Box, Prolog appeared to /be/ magic. It looks like the machine is almost 
/intelligent/ in it's ability to answer question; no wonder people saw 
it and thought that AI would be a solved problem any minute now.

But in fact, it's just a machine following a deterministic decision 
procedure. (It's possible that the human brain fits the same 
description, of course...) Sometimes it seems to pluck answers out of 
the air as if by magic. But other times, it utterly fails to answer 
questions which it looks like it "should" be able to figure out. Because 
it /isn't/ thinking, it's just blindly running a program.

And thus, 40+ years later, we still don't have WOPR, Skynet, HAL, Jonny 
5, Kit or any other similar AI. We don't have anything remotely close to 
it. (I was watching War Games the other day... Christ that film has some 
ancient hardware!)

> Also how hard would it be to add support for arithmetic operators? Then
> you would have an equation solver, which arguably would be more useful.

Yeah, if you've been paying attention, you'll have noticed that 
ultimately everything boils down to equality predicates. There are no 
other comparison operators (e.g., less than or greater than), and there 
are no functions operating on expressions (e.g., no arithmetic).

In a sense, Logic Box /already/ implements arithmetic. If you consider a 
list as representing a number (i.e., the length of the list), then the 
LJoin{} predicate implements addition. AND SUBTRACTION, by the way. 
Because logic programming is like that. And if you implement a predicate 
for performing a Cartesian product of lists [should be hard to do], that 
would implement multiplication. AND DIVISION.

Be careful what you wish for, however: Recall that a 5th-order 
polynomial is potentially impossible to solve. Even limiting ourselves 
to integers, we have Gödel's incompleteness theorems about the 
impossibility of proving statements about integers, and the 
impossibility of Hilbert's tenth problem (it is impossible to even 
decide /if/ a Diophantine equation has /any/ solutions, never mind 
/find/ them).

So yes, I probably can implement some arithmetic into Logic Box. But 
there are limits to what is computable. I'm kinda curious to see how 
that works out...

If you've been paying attention, you'll notice that there's no NOT 
operator. Because how would that work? The equality predicate works by 
adding information until a solution is found or we have to give up, and 
all the other predicates basically work by running equality predicates 
[ultimately]. What would the solution to, say, "NOT x = 5" look like? 
There would have to be some way of representing INequalities in a 
solution. And then we would have to figure out how such inequalities 
combine and so forth.

Adding operators like "less than" or "greater than" would be even 
harder. Logic Box would have to know a bunch of theorems about integers. 
Stuff like "x > 5 & x < 4 is impossible".

I think it would be an interesting project to see what things can or 
cannot be incorporated. But I doubt I'd try to program it as an 
interactive solver; more likely as a batch processing system which gives 
no status information. (That's obviously drastically easier to code.) 
I'd probably do it in Haskell too. (Because then I can spend more time 
concentrating on the theoretical tractability of a confluent set of 
transformation rules, and less time worrying about uncaught class cast 
exceptions due to invariants that the puny Java type system is too 
feeble to enforce...)

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

...and you think I'm doing this because...? ;-)

Post a reply to this message

On 31/05/2012 12:12 PM, Invisible wrote:

> Of course, /the/ canonical logic programming language is Prolog.
> Apparently when people first saw that thing back in the 1970s, everybody
> suddenly thought that human-level AI was just around the corner.

Exhibit A: The Cat from Outer Space, 1978.

In it, the military program in all their data into a truck-sized 
computer with a blurry green screen. They then key in the question "who 
piloted the ship?" The lights flush, the tape streamers go crazy, and 
then the computer slowly replies "the cat".


Exhibit B: War Games, 1983.

The WOPR is a supercomputer that "spends all day thinking about World 
War 3". From the way it behaves, you can just picture it being powered 
by a kind of souped-up Prolog.

By contrast, Tron (1982) comes across as less computerised. The 
characters all behave like humans who are slightly computerised, rather 
than computers that are slightly humanised...

Post a reply to this message

>> 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.

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

Would tell you that x := 2

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

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.

Post a reply to this message

Le 2012-05-31 07:12, Invisible a écrit :
> Of course, /the/ canonical logic programming language is Prolog.
> Apparently when people first saw that thing back in the 1970s, everybody
> suddenly thought that human-level AI was just around the corner.
>

When I first started working int hte mid 90s, there was an "AI Lab" in a 
corner of our building.  It had gotten its name in the 80s, but all it 
really was was an office full of decrepit spare parts for some Motorola 
68000-based system running Prolog and Lisp that was keeping track of 
ground crews at an airport.  Texas Instrument had build this system and 
was trying to market it to airlines who have very complex resource 
planning issues.  Only four airlines had bought the system, so TI 
scrapped it.  Qantas hired all the developpers from TI, Iberia got rid 
of its machines, which were all bought by SwissAir, which left Air 
Canada stuck trying to fix 15 year old hardware to run an airline. 
There's a story of one of our network operators getting on aplane with a 
boot diskette, handing it to the local tehc, and hoping back on the 
return flight, just to restart one of the machines in another city.

Thankfully, Y2K finally forced them to switch to some other (also 
prolog-based) software, but running on less esoteric hardware.

Yeah, I know.  Cool story bro.


-- 
/*Francois Labreque*/#local a=x+y;#local b=x+a;#local c=a+b;#macro P(F//
/*    flabreque    */L)polygon{5,F,F+z,L+z,L,F pigment{rgb 9}}#end union
/*        @        */{P(0,a)P(a,b)P(b,c)P(2*a,2*b)P(2*b,b+c)P(b+c,<2,3>)
/*   gmail.com     */}camera{orthographic location<6,1.25,-6>look_at a }

Post a reply to this message

On 31/05/2012 12:12 PM, Invisible wrote:


>
> It... could. Perhaps. With some serious modifications.
>

[Snip]

Your talents are wasted in your job.

>> Having written something like this is also very good for CVs and job
>> interviews :-)
>
> ....and you think I'm doing this because...? ;-)

You have too much time on your hands and the job that you get paid for 
does not stretch you.

-- 
Regards
     Stephen

Post a reply to this message

On 31/05/2012 02:20 PM, Francois Labreque wrote:

> Yeah, I know. Cool story bro.

The way I heard it, Prolog caused quite a stir when people first saw it 
back in the 1970s. A few simple lines of Prolog gives you a system with 
approximately the apparent logical deductive skills of a 2 year old 
child. And it's really quite a simple piece of programming. The computer 
scientists of the day must surely have thought that in just a few years' 
time, they would have human or super-human intelligence at their 
fingertips...

...and then it didn't actually happen like that, and the "AI winter" 
came along. The scientists promised everybody the Earth, and then 
couldn't deliver, so their funding was slashed.

Post a reply to this message

On 31/05/2012 02:22 PM, Stephen wrote:

> Your talents are wasted in your job.

What? SERIOUSLY??? :-O

>>> Having written something like this is also very good for CVs and job
>>> interviews :-)
>>
>> ....and you think I'm doing this because...? ;-)
>
> You have too much time on your hands and the job that you get paid for
> does not stretch you.

Well, right now - oh, wait, legally I can't tell you about that. Maybe 
in a few weeks' time...

Post a reply to this message

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

On 31/05/2012 11:47 AM, scott wrote:

> Also how hard would it be to add support for arithmetic operators? Then
> you would have an equation solver, which arguably would be more useful.

Peano arithmetic. Basically, you use Z[] to represent 0, and S[x] to 
represent x+1. In this way, 3 is represented by S[S[S[Z[]]]]. (In other 
words, 3 lots of S[].)

It's then quite easy to write sum and product predicates:

ISum{x, y, z}:
   (x = Z[] & y = z) |
   (~px ~pz
     x = S[px] &
     z = S[pz] &
     ISum{px, y, pz}
   )
;

IProduct{x, y, z}:
   (x = Z[] & z = Z[]) |
   (~px ~t
     x = S[px] &
     IProduct{px, y, t} &
     ISum{t, y, z}
   )
;

Using this, I was able to solve the following system of simultaneous 
equations:

   x + y = 9
   2x = y

The first equation can be represented by

   ISum{x, y, nine}

where nine is S[S[S[S[S[S[S[S[S[Z[]]]]]]]]]]. The second equation can be 
written

   IProduct{two, x, y}

where, again, two is S[S[Z[]]].

It takes several thousand steps, but Logic Box finds exactly one solutions:

   x := S[S[S[Z[]]]];
   y := S[S[S[S[S[S[Z[]]]]]]];

In other words, x=3 and y=6, which does solve the given equations.

Notice that the ISum{} predicate on its own gives the solution set

   x := 0; y := 9;
   x := 1; y := 8;
   x := 2; y := 7;
   x := 3; y := 6;
   ...
   x := 8; y := 1;
   x := 9; y := 0;

Note also that the ISum{} predicate needs to come first, since it has a 
finite solution set. The IProduct{} predicate has the infinite solution set

   x := 0; y := 0;
   x := 1; y := 2;
   x := 2; y := 4;
   x := 3; y := 6;
   ...

Either way, the correct solution is located. But if IProduct{} comes 
first, the solver never terminates, fruitlessly searching the infinite 
search space for non-existent further solutions. If ISum{} comes first, 
the search terminates eventually.

Either way, it's pretty damned slow. It's basically searching for all 
possible combinations of numbers having the requested properties.

It shouldn't be too hard to add an IExponent{} predicate too, and ask 
the solver to solve some polynomial equations. Remember, though, that at 
this point it handles only integers.

More generally, I'm going to see whether I can implement some more 
efficient type of arithmetic. (E.g., binary arithmetic.)

Post a reply to this message

On 5/31/2012 5:27, scott wrote:
> 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 saw one discussion of writing a soduko solver with backtracking and etc. 
The guy gave it an empty grid and said "solve this one". And it did.

-- 
Darren New, San Diego CA, USA (PST)
   "Oh no! We're out of code juice!"
   "Don't panic. There's beans and filters
    in the cabinet."

Post a reply to this message

>> 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

Please. I have the source code. And the Git repo. ;-) Nobody else on 
Earth has that...

Post a reply to this message

On 6/2/2012 1:39 PM, Darren New wrote:
> On 5/31/2012 5:27, scott wrote:
>> 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 saw one discussion of writing a soduko solver with backtracking and
> etc. The guy gave it an empty grid and said "solve this one". And it did.
>

It's also pretty trivial to modify the algorithm so that it enumerates 
all the possible solutions from any starting state (or at least tries 
to, if you run on an empty board it'll be listing them for quite a while).

Post a reply to this message

>> Also how hard would it be to add support for arithmetic operators? Then
>> you would have an equation solver, which arguably would be more useful.

> Either way, it's pretty damned slow. It's basically searching for all
> possible combinations of numbers having the requested properties.

> More generally, I'm going to see whether I can implement some more
> efficient type of arithmetic. (E.g., binary arithmetic.)

One might think about implementing some kind of primitive which allows 
you to add and subtract real integers. Actually, this turns out to be 
less helpful than you might imagine.

Using Peano arithmetic, we can write things such as

   x = S[y]

this denotes the fact that x = y+1, without specifying which actual 
integer y contains. We can work that out later. By contrast, if you 
wanted to implement some primitive which works in definite integers, you 
would have to somehow augment the solution language to support 
constraints like "x is one greater than y". Using Peano arithmetic, you 
get that for free.

Perhaps the only primitive I ought to be adding is one to convert 
between real integers and Peano integers...

I did manage to implement addition (and therefore subtraction) of binary 
numbers. On the one hand, that makes numbers much shorter to write. (The 
amount of characters required to represent N is now O(log N) rather than 
O(N).) On the other hand, the predicates become quite a lot more 
complicated, so it's dubious whether it actually runs any /faster/. It's 
also much harder to debug if it doesn't work properly.

Post a reply to this message

> I did manage to implement addition (and therefore subtraction) of binary
> numbers.

The sum of two Peano integers:

ISum{x, y, z}:
   (x = Z[] & y = z) |
   (
     ~predX x = S[predX] &
     ~predZ z = S[predZ] &
     ISum{predX, y, predZ}
   )
;

The sum of two binary integers:

ISum{x, y, z}:
   ~co ~t ISum_Dn{x, y, 0, co, t} &
   (
     (co = 0 & z = t) |
     (co = 1 & z = D[1, t])
   )
;

ISum_D1{x, y, ci, co, z}:
   (x = 0 & y = 0 & ci = 0 & co = 0 & z = 0) |
   (x = 0 & y = 0 & ci = 1 & co = 0 & z = 1) |
   (x = 0 & y = 1 & ci = 0 & co = 0 & z = 1) |
   (x = 0 & y = 1 & ci = 1 & co = 1 & z = 0) |
   (x = 1 & y = 0 & ci = 0 & co = 0 & z = 1) |
   (x = 1 & y = 0 & ci = 1 & co = 1 & z = 0) |
   (x = 1 & y = 1 & ci = 0 & co = 1 & z = 0) |
   (x = 1 & y = 1 & ci = 1 & co = 1 & z = 1)
;

ISum_Dn{x, y, ci, co, z}:
   ~headX ~tailX x = D[headX, tailX] &
   ~headY ~tailY y = D[headY, tailY] &
   ~headZ ~tailZ z = D[headZ, tailZ] &
   (
     (
       tailX = D[] &
       tailY = D[] &
       tailZ = D[] &
       ISum_D1{headX, headY, ci, co, headZ}
     ) |
     (
       ~ct ISum_Dn{tailX, tailY, ci, ct, tailZ} &
           ISum_D1{headX, headY, ct, co, headZ}
     )
   )
;

Note also that if we use Peano integers, there is exactly one way to 
write each number. With binary, there are several ways. For example, 11 
and 0011 both denote 3. The ISum{} predicate above works only for 
numbers containing the same number of bits. I haven't even attempted to 
implement binary multiplication yet. (That would probably turn out to be 
drastically faster, however...)

Post a reply to this message

On 01/06/2012 09:02 AM, Invisible wrote:

> 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...

Heh. So much for that!

Attached is v3, which is a 100% rewrite of the entire codebase. (I mean, 
it's not like it's /large/ or anything...) In particular, you can now 
step /backwards/ as well as forwards. And I've tried to make the status 
display a little less perplexing. (Not sure I succeeded!)

Also, the previous version of this program has a bug relating to named 
predicate calls. Basically, a name capture bug. I believe this new 
version is free of such flaws.

I know how excited everybody has been about this program (i.e., not in 
the slightest), so I imagine this new release will generate a wave of 
excitement...

Post a reply to this message

Attachments:
Download 'logicbox-03 release1.jar.zip' (225 KB)

On 01/06/2012 11:48 AM, Invisible wrote:
> 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...

> 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.

Actually, it turns out that by swapping the order of some predicates, 
you can make it so that Normal Order Reduction is always solution #1. 
This conclusively proves the Turing-completeness of my little 
programming language.

It also conclusively proves something that will surprise nobody: My 
talents are wasted here.

Post a reply to this message