From c62bd85a10681cdb106809e55ff9d29b26302a38 Mon Sep 17 00:00:00 2001
From: grammarware <vadim@grammarware.net>
Date: Sun, 22 Nov 2009 05:46:11 +0000
Subject: [PATCH] typed lambda calculus

git-svn-id: https://slps.svn.sourceforge.net/svnroot/slps@718 ab42f6e0-554d-0410-b580-99e487e6eeb2
---
 topics/exercises/README.txt         |  4 +++-
 topics/exercises/lambda5/Makefile   |  5 +++++
 topics/exercises/lambda5/Syntax.pro | 17 +++++++++++++++++
 topics/exercises/lambda5/Test.pro   |  8 ++++++++
 topics/exercises/lambda5/Typing.pro | 25 +++++++++++++++++++++++++
 5 files changed, 58 insertions(+), 1 deletion(-)
 create mode 100644 topics/exercises/lambda5/Makefile
 create mode 100644 topics/exercises/lambda5/Syntax.pro
 create mode 100644 topics/exercises/lambda5/Test.pro
 create mode 100644 topics/exercises/lambda5/Typing.pro

diff --git a/topics/exercises/README.txt b/topics/exercises/README.txt
index e3b863cc..101ba840 100644
--- a/topics/exercises/README.txt
+++ b/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
 
diff --git a/topics/exercises/lambda5/Makefile b/topics/exercises/lambda5/Makefile
new file mode 100644
index 00000000..c69a8fea
--- /dev/null
+++ b/topics/exercises/lambda5/Makefile
@@ -0,0 +1,5 @@
+none:
+
+test:
+	swipl -f Test.pro
+
diff --git a/topics/exercises/lambda5/Syntax.pro b/topics/exercises/lambda5/Syntax.pro
new file mode 100644
index 00000000..43e9aaf9
--- /dev/null
+++ b/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
+
+
diff --git a/topics/exercises/lambda5/Test.pro b/topics/exercises/lambda5/Test.pro
new file mode 100644
index 00000000..5362791f
--- /dev/null
+++ b/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.
diff --git a/topics/exercises/lambda5/Typing.pro b/topics/exercises/lambda5/Typing.pro
new file mode 100644
index 00000000..fc225e9b
--- /dev/null
+++ b/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).