typed lambda calculus

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

topics/exercises/README.txt

@@ -7,6 +7,8 @@ xml2	- a DCG parser for XML subset (elements and attributes)
 nb1	- abstract syntax for NB
 nb2	- semantics and types for NB
 lambda1	- lambda calculus abstract and concrete syntax in Prolog
-lambda2	- obsolete
+lambda2	- fixed point in lambda calculus
 lambda3 - lambda calculus abstract syntax, free variables, substitution, evaluation
+lambda4 - alpha conversion in lambda calculus
+lambda5 - typed lambda calculus
 

topics/exercises/lambda5/Makefile

@@ -0,0 +1,5 @@
+none:
+
+test:
+	swipl -f Test.pro
+

topics/exercises/lambda5/Syntax.pro

@@ -0,0 +1,17 @@
+% See slide 186
+
+term(var(X)) :- atom(X).
+term(app(T1,T2)) :- term(T1), term(T2).
+term(V) :- val(V).
+
+val(lam(X,XT,T)) :- atom(X), type(XT), term(T).
+val(true).
+val(false).
+
+type(bool).
+type(maps(T1,T2)) :- type(T1), type(T2).
+
+value(lam(X,T)) :- variable(X), term(T).
+value(var(X)) :- variable(X). % pragmatic extension to deal with open terms
+
+

topics/exercises/lambda5/Test.pro

@@ -0,0 +1,8 @@
+:- ['Typing.pro'].
+
+%
+% Testing typing rules; see slide 165
+%
+:- 
+ hastype([],app(lam(f,maps(bool,bool),app(var(f),false)),lam(g,bool,var(g))),T),
+ write(T), nl.

topics/exercises/lambda5/Typing.pro

@@ -0,0 +1,25 @@
+% 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,XT,T),maps(XT,U)) :-
+ hastype([[X,XT]|G],T,U).
+
+% T-Application
+hastype(G,app(T,U),Type) :-
+ hastype(G,U,UT),
+ hastype(G,T,maps(UT,Type)).
+
+% See slide 184
+
+% T-True
+hastype(_,true,bool).
+
+% T-False
+hastype(_,false,bool).