β-reduction implemented in Prolog

% Beta reduction  Using free renamimg of variables to avoid capture
% (and no garbage collection)

:-op(180,fx,'\'). %abstraction- for reading only
:-op(170,yfx,'@'). %application
:-op(200,xfx,:).   % real abstraction op.
:-op(400,xfy,'>>'). % reduce with counter for fresh variables
:-op(400,xfy,'=>'). % reduce

:-op(160,xfy,'^').  % exponents
:-op(200,xfy,'$').  % products
:-op(250,xfy,'#').  % sums

beta 2

Normal forms

%  Utility predicates
%****************
nnum(0).
nnum(X):-nnum(Y),X is Y+1.
append([],L,L).
append([H|Tl],L,[H|Ntl]):-append(Tl,L,Ntl).
%******* normality**********
normal(X):-variable(X).
normal(U @ V @ W):-normal(U @ V),normal(W).
normal(X @ V):-variable(X),normal(V).
normal(\X:U):-variable(X),normal(U).
makevar(N,X):-number_chars(N,M),name(X,[120|M]).
make_variable(X):-nnum(N),makevar(N,X).
variable(X):-atom(X).

Graft

%****************************************************************
%  "substitution" allowing capture
plug_in(X,U,V@W,B1@B2) :- plug_in(X,U,V,B1),plug_in(X,U,W,B2),!.
plug_in(X,U,\X:M,\X:M) :- !.
plug_in(X,U,\Y:M,\Y:N) :- X\==Y,plug_in(X,U,M,N),!.
plug_in(X,U,X,U) :- variable(X),!.
plug_in(X,U,Y,Y) :- variable(X),variable(Y),X\==Y,!.

renaming

  %****************Rename: name is assumed fresh!****************
ren(N,X,N,X):-variable(X),!.
ren(N,U@V,K,U1@V1) :- ren(N,U,M,U1),ren(M,V,K,V1),!.
ren(N,\X:U,M,\W:U1) :- makevar(N,W),plug_in(X,W,U,V),
        N1 is N+1,ren(N1,V,M,U1),!.
subn(N,N,X,U,X,U):-variable(X),!.
subn(N,N,X,U,Y,Y):-variable(X),variable(Y),X\==Y,!.
subn(N,M,X,U,V@W,V1@W1):-subn(N,N1,X,U,V,V1),subn(N1,M,X,U,W,W1),!.
subn(N,K,Y,U,\Y:V,\Y:V):-variable(Y),!.
subn(N,K,Y,U,\X:V,\W:B):-X\==Y,ren(N,\X:V,K1,\W:V1),
        subn(K1,K,Y,U,V1,B),!.
sub(X,U,V,W):-subn(0,_,X,U,V,W),!.

beta 5

reduction with counters

  %****************reduction with counters for fresh variables.
c_term(Counter,X) >> c_term(Counter,X) :- variable(X),!.
c_term(Counter,X) >> c_term(Counter,X) :- normal(X),!.
c_term(Counter,(\X:V)@U)  >>  c_term(NewCounter,W) :-
        subn(Counter,Counter1,X,U,V,B),
        c_term(Counter1,B) >> c_term(NewCounter,W),!.
c_term(Counter,U@W)  >>  c_term(NewCounter,B) :-
        c_term(Counter,U)  >>  c_term(Counter1,U1),
        c_term(Counter1,W) >> c_term(Counter2,W1),
        c_term(Counter2,U1 @ W1)  >> c_term(NewCounter,B),!.
c_term(Counter,\X:V)  >>  c_term(NewCounter,\X:W) :-
        c_term(Counter,V)  >>  c_term(NewCounter,W),!.
%********** REDUCTION ************
U => V :- c_term(0,U) >> c_term(_,V).

beta 6

arithmetic handlers

  %****************************************************************
%    user i/o for arithemetic
pre_num2church(0,x).
pre_num2church(N,f@U):-N>0,M is N-1,pre_num2church(M,U).
num2church(N,\f:(\x:U)) :- pre_num2church(N,U).
ch2num(\F:(\X:U),N) :- pre_ch2num(X,F,U,N).
pre_ch2num(X,F,F@U,N):-pre_ch2num(X,F,U,M),N is M+1.
pre_ch2num(X,F,X,0):-variable(X).
church2num(A,B) :- ch2num(A,B).

beta 7

library

  % true y false
true(\x:(\y:x)).
false(\x:(\y:y)).
% cero
cero(\f:(\x:x)).
sucesor(\z:(\f:(\x:(f@(z@f@x))))).
sum(\a:(\b:(\f:(\x: a@f@(b@f@x))))).
%****************
prod(\a:(\b:(\c:a@(b@c)))).
exp(\a:(\b:(b@a))).

beta 8

lib (cont).

add(M,N,V):-num2church(M,Cm),num2church(N,Cn),sum(S),
        S@Cm@Cn=>Lambda_sum,ch2num(Lambda_sum,V).
times(M,N,V):-num2church(M,Cm),num2church(N,Cn),prod(S),
        S@Cm@Cn=>Lambda_prod,ch2num(Lambda_prod,V).
power(M,N,V):-num2church(M,Cm),num2church(N,Cn),exp(S),
        S@Cm@Cn=>Lambda_exp,ch2num(Lambda_exp,V).

eval(X,X):-number(X).
eval(A#B,C):-eval(A,A1),eval(B,B1),add(A1,B1,C).
eval(A$B,C):-eval(A,A1),eval(B,B1),times(A1,B1,C).
eval(A^B,C):-eval(A,A1),eval(B,B1),power(A1,B1,C).

contrib

  /* Courtesy of: Alejandro J. Garcia, Agosto de 1996 */
%**************** el combinador de punto fijo de Church
% que tiene la propiedad:
%
%       M(TM) =(beta) TM
% y(T) devuelve el lambda terminto Y generador de puntos fijos
y( \f:( (\x:(f@(x@x))) @ ((\x:(f@(x@x)))) )  ).
%***el combinador de punto fijo _T_de Turing, que tiene la propiedad:
%
%       M(TM) => TM
turing((\z:(\f:f@(z@z@f)))@(\z:(\f:f@(z@z@f)))).
% malo(T) devuelve el lambda termino malo (\x.xx)(\x.xx)
malo(  (\x:(x@x))  @ (\x:(x@x))  ).

beta 10

predecessor

pred(\x: (x @ M @ N)@False) :-
            predm(M),predn(N),cero(False).
predm(\p:(\u:(u @ (SUCC @ (p @ TRUE)) @ (p @ TRUE))))  :-
        sucesor(SUCC),true(TRUE).
predn(\u:( u @ OH @ OH)) :- cero(OH).