polishing code & references after the lab

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

topics/exercises/lambda4/Test.pro

@@ -42,7 +42,7 @@
  Fix = lam(f,app(lam(x,app(var(f),lam(y,app(app(var(x),var(x)),var(y))))),lam(x,app(var(f),lam(y,app(app(var(x),var(x)),var(y))))))), % CBV
  F = lam(e,lam(x,if(iszero(var(x)),true,if(iszero(pred(var(x))),false,app(var(e),pred(pred(var(x)))))))),
  IsEven = app(Fix,F),
- manysteps(app(IsEven,3),Q4),
+ manysteps(app(IsEven,257),Q4),
  write(Q4), nl,
 
  halt.

topics/exercises/lambda5/Substitution.pro

@@ -8,16 +8,16 @@ 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,M),lam(X,M)).
-substitute(N,X,lam(Y,M1),lam(Y,M2)) :-
+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,M1),lam(Z,M3)) :-
+substitute(N,X,lam(Y,T,M1),lam(Z,T,M3)) :-
   \+ X == Y,
   fv(N,Xs),
   member(Y,Xs),

topics/exercises/lambda5/Test.pro

@@ -2,16 +2,18 @@
 :- ['Evaluation.pro'].
 
 %
-% Testing typing rules; see slide 165
+% 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),

topics/exercises/while5/Types.pro

@@ -3,7 +3,7 @@
 % type(Expression,DeclaredIn,DeclaredOut,Type), where Type = unit
 % type(Expression,Declared,Type), where Type = bool or nat
 
-%% StateDents have the 'unit' type
+%% StateDents have the 'unit' type, see slide 191
 type(slist(S1,S2),D1,D2,U) :-
  wtype(S1,D1,D3,unit),
  wtype(S2,D3,D2,U).