[CST-2] Types

[Peter Taylor]

> Just a wee question on PLC datatypes.  1998 Paper 7 Question 10 - the
> second part basically asks for a PLC representation of the successor
> function - s(n) = n+1.  This is probably very easy, but I'm just not sure
> how to encode the addition of 1 in PLC, is this actually significant as
> it doesn't alter the type?  Very confused.

What you want is (s n) x f = f^(n+1)(x) from defn
So (s n) x f = f (n x f).
Curry thrice to get
s = lambda n. lambda x. lambda f. f(n x f)
with appropriate types for the bound variables.

Peter
=====
Peter Taylor
pjt33@cam.ac.uk