Home » forums » LtU Forum

SK in Prolog

A thought experiment I am too lazy to do so I'll ask you folk.

Define SK, define a reduction relation, ask whether two terms are equal/reduce to similar terms.

Can you do this in Prolog? (Asked because of interest in current unification based languages like miniKanren.)

By marco at 2017-09-08 15:39 | LtU Forum | previous forum topic | next forum topic | other blogs | 3588 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I programmed a bit anyway, not sure I got it right.

% Ix = x
% (Kx)y = x
% ((Sx)y)z = xz(yz)

term(s).  term(k).  term(i).
term(app(X, Y)) :- term(X), term(Y).

step(app(i, X), X) :- term(X).
step(app(app(k, X), Y), X) :- term(X), term(Y).
step(app(app(app(s, X), Y), Z), app(app(X, Z), app(Y, Z))) :- term(X), term(Y), term(Z).

reduce(X, Y) :- step(X, Y).
reduce(app(X, Y), app(X0, Y)) :- reduce(X, X0).
reduce(app(X, Y), app(X, Y0)) :- reduce(Y, Y0).

It can do some trivial stuff like program derivation, for example, everything which reduces to 'I', but I am not sure I got the relation exactly right. Neither am I sure that Prolog explores the state space in a very intelligent manner.

But, ah well, maybe people can make use of it.

By marco at Fri, 2017-09-08 19:52 | login or register to post comments

Iterative deepening

The depth first search easily gets stuck in loops. Breadth first is more useful for enumerating all solutions, however it has a memory efficiency problem.

Iterative deepening is a good compromise, as each pass is as memory efficient as depth first, and although less time efficient, it is bounded by the fanout of the search space. If the Prolog implementation can limit the search depth you can easily write a script to do iterative deepening.

There were a few papers written about using Prolog as a theorem prover (Prolog Technology Theorem Prover). There are three key areas that need to be "fixed" to do this:

- incomplete search strategy (fixed by using iterative deepening for example).
- unsound unification (make sure using occurs check).
- incomplete inference (add model elimination).

The first two are trivial, the third took me a long time to understand, and got me side-tracked on the nature of negation for a while. I think I have finally understood that existential quantification is essential for negation (if we are thinking of negation as a program rewrite). I haven't quite understood how all this relates back to model elimination yet.

By Keean Schupke at Sun, 2017-09-10 07:05 | login or register to post comments

Cannot

Determining whether two arbitrary terms are equal in a Turing-complete calculus is a superset to solving the Halting problem, is it not?

By dmbarbour at Fri, 2017-09-08 20:33 | login or register to post comments

Depends on equal

Some systems are confluent and then syntactic equality on what terms reduce to is simple. But in the general case, it is undecidable, yes. (I am not very clear here but this is all a) long ago for me and b) not in any way my expertise. But I expect that there is a small but significant difference between "do these two terms rewrite to the same term" and "do these two terms given a value always rewrite to the same term." Right?)

Uhm. I am sorry, I was a bit sloppy in my terminology in the topic. This was what I was interested in since I wanted a system which can do miniKanren stuff in Prolog.

It does answer queries like "reduce(X, i)." (all terms which reduce to 'I') and "reduce(X, Z), reduce(Y,Z)" (all terms which reduce to the same term) but it is a bit dumb in the way it searches the state space.

I am pretty sure the program above can easily be extended to query undecidable problems.

By marco at Fri, 2017-09-08 21:11 | login or register to post comments

I expect that there is a

I expect that there is a small but significant difference between "do these two terms rewrite to the same term" and "do these two terms given a value always rewrite to the same term." Right?

That sounds right. Except for the "small but" qualifier.

For example, there's an infinite number of ways you can write the fixpoint function. And hence every `fixk fib` will be distinct for most values of `k`. But for all of them, `fixk fib 7` should evaluate to `13` (assuming `fib` is equivalent to `fun f x -> if(x < 2) then 1 else f (x-1) + f (x-2)`). If the "term" is just the syntax, then it's trivial to compare terms for equality. But we'll need to accept that `fixk fib` is not equal to `fixk+1 fib` even though they're equal under every observation within the system.

Interestingly, there are infinite fixpoint functions that, instead of being simple quines (where the fix function rewrites to itself internally, and you can observe this a the syntactic layer), you can have cyclic rotations or fractal expansions of fixpoint terms. It is generally difficult to determine when two terms are part of the same cycle or fractal expansion.

By dmbarbour at Fri, 2017-09-08 23:45 | login or register to post comments