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