Jason (jcreed) wrote,
Jason
jcreed

The following appears to be an adequate encoding of the untyped lambda calculus in Standard ML:

datatype ('a,'b) term = T of
('b -> 'a)
* ('a * 'a -> 'a)
* (('a,('b option)) term -> 'a)
-> 'a

datatype void = V of void

type 'a tm = ('a, void) term

Every value at type 'a tm should correspond to an untyped lambda term.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments