lab preparations (+ bug fixes)

git-svn-id: https://slps.svn.sourceforge.net/svnroot/slps@726 ab42f6e0-554d-0410-b580-99e487e6eeb2

topics/exercises/README.txt

@@ -13,4 +13,5 @@ lambda2	 - lambda caclulus with Church numbers
 lambda3  - lambda calculus abstract syntax, free variables, substitution, evaluation
 lambda4	 - untyped lambda calculus with alpha conversion & fixed point combinator
 lambda5  - typed lambda calculus with alpha conversion
+lambda6  - typed lambda calculus with alpha conversion & fixed point operator
 

topics/exercises/lambda5/FV.pro

@@ -9,7 +9,7 @@ fv(app(M,N),FV) :-
   fv(N,FV2),
   union(FV1,FV2,FV).
 
-fv(lam(X,M),FV) :-
+fv(lam(X,_,M),FV) :-
   fv(M,FV1),
   subtract(FV1,[X],FV).
 

topics/exercises/lambda5/Makefile

@@ -3,3 +3,5 @@ none:
 test:
 	swipl -f Test.pro
 
+clean:
+	rm -f *~

topics/exercises/lambda5/Test.pro

@@ -19,8 +19,8 @@
  hastype([],F,T3),
  write(T3), nl,
  IsEven = fix(F),
- hastype([],IsEven,T4),
- write(T4), nl,
+% hastype([],IsEven,T4),
+% write(T4), nl,
 % manysteps(app(IsEven,3),Q),
 % write(Q), nl,
  halt.

topics/exercises/lambda5/Typing.pro

@@ -35,4 +35,5 @@ hastype(G,if(T1,T2,T3),Type) :-
 
 % Fixed point combinator, see slide 189
 % Typing rule
-hastype(G,fix(T),Type) :- hastype(G,T,maps(Type,Type)).
+% hastype(G,fix(T),Type) :- ...
+

topics/exercises/lambda6/Evaluation.pro

@@ -0,0 +1,78 @@
+%
+% See slide 174
+%
+% Note the use of meta-variables in the formal notation.
+% Those meta-variables must be mapped to extra literals as shown below.
+%
+
+:- ['Syntax.pro'].
+:- ['Substitution.pro'].
+
+
+% One-step transition relation
+
+% see slide 189
+onestep(fix(T1),fix(T2)) :-
+ onestep(T1,T2).
+
+onestep(fix(lam(X,XT,T1)),T2) :-
+ substitute(fix(lam(X,XT,T1)),X,T1,T2).
+
+onestep(app(T1,T2),app(T3,T2)) :-
+  onestep(T1,T3).
+
+onestep(app(V,T1),app(V,T2)) :-
+  value(V),
+  onestep(T1,T2).
+
+onestep(app(lam(X,_,T1),V),T2) :-
+  value(V),
+  substitute(V,X,T1,T2).
+
+
+% Extension to deal with Prolog numbers and Booleans
+
+onestep(succ(T1),succ(T2)) :- 
+  onestep(T1,T2).
+
+onestep(succ(V1),V2) :- 
+  value(V1),
+  V2 is V1 + 1.
+
+onestep(pred(T1),pred(T2)) :- 
+  onestep(T1,T2).
+
+onestep(pred(V1),V2) :- 
+  value(V1),
+  V2 is V1 - 1.
+
+onestep(iszero(T1),iszero(T2)) :- 
+  onestep(T1,T2).
+
+onestep(iszero(V),true) :- 
+  value(V),
+  V == 0.
+
+onestep(iszero(V),false) :- 
+  value(V),
+  \+ V == 0.
+
+onestep(if(T1,T2,T3),if(T4,T2,T3)) :- 
+  onestep(T1,T4).
+
+onestep(if(true,T,_),T).
+
+onestep(if(false,_,T),T).
+
+% Fixed point (recursion)
+% Evaluation rules from slide 189
+% onestep(fix(T1),T2) :- ...
+
+% Reflexive, transitive closure
+
+manysteps(V,V) :-
+  value(V).
+
+manysteps(T1,T3) :- 
+  onestep(T1,T2),
+  manysteps(T2,T3).

topics/exercises/lambda6/FV.pro

@@ -0,0 +1,26 @@
+% See slide 153
+
+:- ['Syntax.pro'].
+
+fv(var(X),[X]).
+
+fv(app(M,N),FV) :-
+  fv(M,FV1),
+  fv(N,FV2),
+  union(FV1,FV2,FV).
+
+fv(lam(X,_,M),FV) :-
+  fv(M,FV1),
+  subtract(FV1,[X],FV).
+
+fv(fix(X),FV) :- fv(X,FV).
+
+% Extension to deal with Prolog numbers and Booleans
+
+fv(true,[]).
+fv(false,[]).
+fv(N,[]) :- number(N).
+fv(pred(M),FV) :- fv(M,FV).
+fv(succ(M),FV) :- fv(M,FV).
+fv(iszero(M),FV) :- fv(M,FV).
+fv(if(M1,M2,M3),FV) :- fv(M1,FV1), fv(M2,FV2), fv(M3,FV3),   union(FV1,FV2,FV4), union(FV4,FV3,FV).

topics/exercises/lambda6/Makefile

@@ -0,0 +1,7 @@
+none:
+
+test:
+	swipl -f Test.pro
+
+clean:
+	rm -f *~

topics/exercises/lambda6/Substitution.pro

@@ -0,0 +1,61 @@
+% See slide 157
+
+:- ['Syntax.pro'].
+:- ['FV.pro'].
+
+substitute(N,X,fix(F1),fix(F2)) :-
+  substitute(N,X,F1,F2).
+substitute(N,X,var(X),N).
+substitute(_,X,var(Y),var(Y)) :- \+ X == Y.
+substitute(N,X,app(M1,M2),app(M3,M4)) :-
+  substitute(N,X,M1,M3),
+  substitute(N,X,M2,M4).
+substitute(_,X,lam(X,T,M),lam(X,T,M)).
+substitute(N,X,lam(Y,T,M1),lam(Y,T,M2)) :-
+  \+ X == Y,
+  fv(N,Xs),
+  \+ member(Y,Xs),
+  substitute(N,X,M1,M2).
+
+% Special case for alpha conversion
+
+substitute(N,X,lam(Y,T,M1),lam(Z,T,M3)) :-
+  \+ X == Y,
+  fv(N,Xs),
+  member(Y,Xs),
+  freshvar(Xs,Z),
+  substitute(var(Z),Y,M1,M2),
+  substitute(N,X,M2,M3).
+
+% Extension to deal with Prolog numbers and Booleans
+
+substitute(_,_,true,true).
+substitute(_,_,false,false).
+substitute(_,_,N,N) :- number(N).
+substitute(N,X,succ(M1),succ(M2)) :-
+  substitute(N,X,M1,M2).
+substitute(N,X,pred(M1),pred(M2)) :-
+  substitute(N,X,M1,M2).
+substitute(N,X,iszero(M1),iszero(M2)) :-
+  substitute(N,X,M1,M2).
+substitute(N,X,if(M1,M2,M3),if(M4,M5,M6)) :-
+  substitute(N,X,M1,M4),
+  substitute(N,X,M2,M5),
+  substitute(N,X,M3,M6).
+
+%
+% freshvar(Xs,X): X is a variable not in Xs.
+% We use numbers as generated variables.
+% Variables and numbers can still not be confused (because variables are wrapped in var(...)). 
+%
+
+freshvar(Xs,X) :-
+  freshvar(Xs,X,0).
+
+freshvar(Xs,N,N) :- 
+  \+ member(N,Xs).
+
+freshvar(Xs,X,N1) :- 
+  member(N1,Xs),
+  N2 is N1 + 1,
+  freshvar(Xs,X,N2).

topics/exercises/lambda6/Syntax.pro

@@ -0,0 +1,38 @@
+% See slide 186
+
+term(X) :- value(X).
+term(var(X)) :- variable(X).
+term(app(T1,T2)) :- term(T1), term(T2).
+
+% Primitive fixed point combinator, see slide 189
+term(fix(T)) :- term(T).
+
+% Extension to deal with Prolog numbers and Booleans
+
+term(succ(T)) :- term(T).
+term(pred(T)) :- term(T).
+term(iszero(T)) :- term(T).
+term(if(T1,T2,T3)) :- term(T1), term(T2), term(T3).
+
+% Types
+
+type(bool).
+type(nat).
+type(maps(T1,T2)) :- type(T1), type(T2).
+
+% Normal forms
+
+value(lam(X,XT,T)) :- variable(X), type(XT), term(T).
+
+% Extension to deal with Prolog numbers and Booleans
+
+value(true).
+value(false).
+value(X) :- number(X).
+
+/*
+ We use atomic/1 so that we can use numbers for "generated" vars.
+ This is needed for alpha conversion in substitution.
+*/
+
+variable(X) :- atomic(X).

topics/exercises/lambda6/Test.pro

@@ -0,0 +1,26 @@
+:- ['Typing.pro'].
+:- ['Evaluation.pro'].
+
+%
+% Testing typing rules
+%
+:- 
+ % taken from slide 185
+ % |-  (λf:bool→bool . f false) λg:bool . g  :  bool
+ hastype([],app(lam(f,maps(bool,bool),app(var(f),false)),lam(g,bool,var(g))),T1),
+ write(T1), nl,
+ % |-  λx:nat . λy:nat if x==0 then succ(x) else pred(y)  :  nat
+ If = lam(x,nat,lam(y,nat,if(iszero(var(x)),succ(var(x)),pred(var(y))))),
+ hastype([],If,T2),
+ write(T2), nl,
+ % taken from slide 190
+ % |-  λe:nat→bool . λx:nat if x==0 then true else if (pred x)==0 then false else (e (pred pred x))  :  (nat→bool)→nat→bool
+ F = lam(e,maps(nat,bool),lam(x,nat,if(iszero(var(x)),true,if(iszero(pred(var(x))),false,app(var(e),pred(pred(var(x)))))))),
+ hastype([],F,T3),
+ write(T3), nl,
+ IsEven = fix(F),
+ hastype([],IsEven,T4),
+ write(T4), nl,
+ manysteps(app(IsEven,3),Q),
+ write(Q), nl,
+ halt.

topics/exercises/lambda6/Typing.pro

@@ -0,0 +1,38 @@
+%% Type system for lambda calculus, see slide 183
+:- ['Syntax.pro'].
+
+% hastype(Context,Term,Type)
+
+% T-Variable
+hastype(G,var(V),Type) :-
+ member([V,Type],G).
+
+% T-Abstraction
+hastype(G,lam(X,Type,T),maps(Type,U)) :-
+ hastype([[X,Type]|G],T,U).
+
+% T-Application
+hastype(G,app(T,U),Type) :-
+ hastype(G,U,UT),
+ hastype(G,T,maps(UT,Type)).
+
+%% Booleans, see slide 184
+% T-True
+hastype(_,true,bool).
+
+% T-False
+hastype(_,false,bool).
+
+% Naturals
+hastype(_,X,nat) :- number(X).
+hastype(G,succ(T),nat) :- hastype(G,T,nat).
+hastype(G,pred(T),nat) :- hastype(G,T,nat).
+hastype(G,iszero(T),bool) :- hastype(G,T,nat).
+hastype(G,if(T1,T2,T3),Type) :-
+  hastype(G,T1,bool),
+  hastype(G,T2,Type),
+  hastype(G,T3,Type).
+
+% Fixed point combinator, see slide 189
+% Typing rule
+hastype(G,fix(T),Type) :- hastype(G,T,maps(Type,Type)).