Lambda Calculus in PROLOG

[Graham Cooper]

This is a simple method using a single parameter.


x = reserved term
X = reserved VAR

f( EXPRESSION, X , REDUCTION )

f( plus(x,Y) , X , plus(X,Y) ).


*********


?- f( plus(x,6) , 5 , ANS ).


ANS = plus(5,6)



----------------

Chuck that LISP out of PROLOG ! ! bagOf all over again!


Herc
--
www.BLoCKPROLOG.com (b)eta

[Graham Cooper]

On May 24, 12:45 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> This is a simple method using a single parameter.
>
> x = reserved term
> X = reserved VAR
>
> f(  EXPRESSION, X , REDUCTION )
>
> f(  plus(x,Y) , X , plus(X,Y) ).
>
> *********
>
> ?- f( plus(x,6) , 5 , ANS ).
>
> ANS = plus(5,6)
>
> ----------------
>

I tried 2-variable lambda expression reduction using only UNIFY.

This is basic MOD 3 Arithmetic, but these operands could just shell
over built in functions.

e.g.

lambda x,y (0+2) [] [] = 2 | THEN HALT


lxy( plus( 0 , 0 ) , n , n , 0 , halt).
lxy( plus( 0 , 1 ) , n , n , 1 , halt).
lxy( plus( 0 , 2 ) , n , n , 2 , halt).

lxy( plus( 1 , 0 ) , n , n , 1 , halt).
lxy( plus( 1 , 1 ) , n , n , 2 , halt).
lxy( plus( 1 , 2 ) , n , n , 0 , halt).

lxy( plus( 2 , 0 ) , n , n , 2 , halt).
lxy( plus( 2 , 1 ) , n , n , 0 , halt).
lxy( plus( 2 , 2 ) , n , n , 1 , halt).

lxy( mult( 0 , 0 ) , n , n , 0 , halt).
lxy( mult( 0 , 1 ) , n , n , 0 , halt).
lxy( mult( 0 , 2 ) , n , n , 0 , halt).

lxy( mult( 1 , 0 ) , n , n , 0 , halt).
lxy( mult( 1 , 1 ) , n , n , 1 , halt).
lxy( mult( 1 , 2 ) , n , n , 2 , halt).

lxy( mult( 2 , 0 ) , n , n , 0 , halt).
lxy( mult( 2 , 1 ) , n , n , 2 , halt).
lxy( mult( 2 , 2 ) , n , n , 1 , halt).

lxy( plus(x,y) , X , Y , plus(X,Y) , Z ).

lxy( plus(x,R) , X , Y , plus(X,R) , z(Z) )
:- lxy( SUB , n , Y , R , Z ).


This is not quite right, here I push down variable Y
to a sub lambda expression and instantiate X.




lxy( plus(L,R) , X , Y , plus(TRM1,TRM2) , z(Z) )
:- lxy( SUBL , X , Y , TRM1 , Z ),
lxy( SUBR , X , Y , TRM1 , Z ).

lxy( mult(x,y) , X , Y , mult(X,Y) , Z ).

lxy( mult(x,R) , X , Y , mult(X,R) , z(Z) )
:- lxy( SUB , X , Y , R , Z ).

lxy( mult(L,R) , X , Y , mult(TRM1,TRM2) , z(Z) )
:- lxy( SUBL , X , Y , TRM1 , Z ),
lxy( SUBR , X , Y , TRM1 , Z ).

?- lxy( plus(x,1) , 1 , n , ANS, z(halt)).

?- lxy( plus( mult(1,1) , mult(2,1) ) , n , n , ANS , z(halt) ).

?- lxy( plus( mult(x,1) , mult(1,y) ) , 2 , 1 , ANS , z(z(halt)) ).




--------------

This is still buggy, but what it should do is..


?- lxy( plus(mult(1,x), mult(2,y) , 2 , 1 , ANS , z(z(z(z(halt)))) )


ANS = plus(mult(1,2),mult(2,1) , n , n , .., z(z(halt))

= plus(2,2) , n , n , .., z(halt)

= 4 halt


i.e. a depth limited reduction calculator.



---------------

but the combinations of x,y,X,Y was starting to be a problem.

so I think to do lambda style calculations a high order currying
system is more suited for fixed arity platform.


lx( EXPRESSION , [x | y,z] , REDUCTION , timeout )


which reduces one argument at a time.

-->

lx( REDUCTION , [ y | z ] , REDUCTION2 , smaller-timeout ).


-------------

But that's all the time I'll spend on a lambda calculator, for now!

The technique is just to encode structured expressions instead of
strings, then native unify can do the binding for you.

Herc
--
www.BLoCKPROLOG.com