Solutions to Problems 3-6 from PS6 are included at the end.

***********************************************************************
* A Denotational Semantics Interpreter for the Lambda Calculus,       *
* from Chapter 10 of Reynolds.                                        *
***********************************************************************

Written by Paul Hudak.

> module LCInterpreter where

SYNTAX
======

> data Exp = Var String      -- variables
>          | App Exp Exp     -- applications
>          | Lam String Exp  -- abstractions
>      deriving (Eq, Show)

SEMANTIC DOMAINS
================

Reynolds defines a domain isomorphism:

Dinf ~ (Dinf -> Dinf)

with the pair of injection/projection functions:

phi :: Dinf -> (Dinf -> Dinf)
psi :: (Dinf -> Dinf) -> Dinf

He treats the domain very abstractly, and claims that its construction
is beyond the scope of the text.

However, suppose we wish to to prototype the denotational semantics in
Haskell?  How do we construct a datatype corresponding to Dinf?

We can get at an answer by asking a more fundamental question: what is
the meaning of a term in the lambda calculus?  From everything
discussed about reduction semantics, it seems that the operational
meaning of a term is a term in normal form, or no term at all in the
case of divergence.  So let's try to mimick that idea by creating a
Haskell datatype for normal forms.  Remember that a normal form is a
lambda term with no beta redexes.  This leads to:

> data Dinf   = NoBeta NoBeta
>             | Fn (Dinf -> Dinf)
>
> data NoBeta = Vr String
>             | Ap NoBeta Dinf

data NF = NoLam NoLam
        | Lm String NF

data NoLam = Vr String
           | App NoLam NF

Note the mutual recursive nature of these data types.  (Note also that
this solution is reminiscent of higher-order abstract syntax.)

We can define the pair of coercion functions phi and psi as follows:

> phi :: Dinf -> (Dinf -> Dinf)
> phi (NoBeta nb) = \d -> NoBeta (Ap nb d)
> phi (Fn f)     = f
>
> psi :: (Dinf -> Dinf) -> Dinf
> psi = Fn

phi and psi are "almost" inverses.  Everything works fine in this
direction:

  phi . psi = id:
  phi (psi f) = phi (Fn f) = f

In the other direction everything works fine with functions:

  psi . phi = id:
  psi (phi (Fn f)) = psi f = Fn f

but with NoBeta's we get the following:

  psi (phi (NoBeta nb)) 
  = psi (\d -> NoBeta (Ap nb d))
  = Fn (\d -> NoBeta (Ap nb d))
  = Fn (NoBeta . Ap nb)

This is not completely satisfactory, but makes sense intuitively, in
that the equivalence of (NoBeta nb) and (Fn (NoBeta . Ap nb)) is a
kind of eta-conversion.  (The fact that these are distinguished in
Dinf will mean that eta-conversion is not sound in the semantics.)

ENVIRONMENTS
============

> type Env = String -> Dinf
>
> extend :: Env -> String -> Dinf -> Env
> extend eta v d v' = if v == v' then d else eta v'

DENOTATIONAL SEMANTICS
======================

With the above preliminaries, the denotational semantics is completely
straightforward and precisely mimicks that in the text:

> red :: Exp -> Env -> Dinf
>
> red (Var s) eta     = eta s
> red (App e0 e1) eta = phi (red e0 eta) (red e1 eta)
> red (Lam v e) eta   = psi (\x -> red e (extend eta v x))

PRINTER
=======

The function "red" is essentially a normal-order lambda calculus
reducer, but is based on the denotational semantics rather than the
reduction semantics.  In order to display the result, we have to
figure out how to display values in Dinf.  The tricky part is
"reconstructing" lambda terms from values in (Dinf -> Dinf).  The
following function achieves that by passing a "fresh" name supply
around from which new variables can be created.  (The variable supply
should not include any free variables in the term being shown, but
here I have been lazy and left that part out.)

> vars :: [String]
> vars = ["a","b","c","d","e","f","g","h","i","j","k"]

> showDinf :: Dinf -> String
> showDinf d = fst (sdf d vars)

> sdf :: Dinf -> [String] -> (String, [String])
> sdf (NoBeta (Vr s))    vs = (s, vs)
> sdf (NoBeta (Ap nb d)) vs = 
>   let (snb, vs') = sdf (NoBeta nb) vs
>       (sd, vs'') = sdf d vs'
>   in ("(" ++ snb ++ " " ++ sd ++ ")", vs'')
> sdf (Fn f) (v:vs) = 
>   let (s, vs') = sdf (f (NoBeta (Vr v))) vs
>   in ("(\\" ++ v ++ "-> " ++ s ++ ")", vs')

TEST HARNESS
============

An initial environment that maps every variable to itself:

> eta0 :: Env
> eta0 v = NoBeta (Vr v)

A test function that reduces a term in the initial environment, then
"shows" the result:

> doit :: Exp -> IO ()
> doit e = putStr (showDinf (red e eta0))

EXAMPLES
========

A free variable:

> e0 = Var "x"

The identity combinator:

> e1 = Lam "x" (Var "x")

The self-application combinator:

> e2 = Lam "x" (App (Var "x") (Var "x"))

An application with a beta redex:

> e3 = App e1 e2

A test of name capture:

> e4 = App (Lam "x" (Lam "y" (Var "x"))) (Var "y")

A free variable under a lambda:

> e5 = Lam "x" (Var "y")

A redex under a lambda:

> e6 = Lam "z" e3

Note that eta contraction fails (precisely because phi and psi are
only "almost" inverses):

> e7 = Lam "x" (App (Var "y") (Var "x"))

------------------------------------------------------------------

Solutions to PS6 (and more)
---------------------------

3) Using the lambda calculus interpreter provided below, implement
TRUE, FALSE, NUMn (for 0 <= n <= 10), ISZERO, SUCC, ADD, and MULT as
defined in Section 10.6.  Test your implementation.
 
TRUE and FALSE:

> true  = Lam "x" (Lam "y" (Var "x"))
> false = Lam "x" (Lam "y" (Var "y"))

Numbers:

> num0  = Lam "f" (Lam "x" (Var "x"))
> num1  = App suc num0
> num2  = App suc num1
> num3  = App suc num2
> num4  = App suc num3
> num5  = App suc num4
> num6  = App suc num5
> num7  = App suc num6
> num8  = App suc num7
> num9  = App suc num8
> num10 = App suc num9

ISZERO:

> isZero = Lam "n" (Lam "x" (Lam "y" 
>            (App (App (Var "n") (Lam "z" (Var "y"))) (Var "x"))))

SUCC, ADD, MULT, and EXP:

> suc = Lam "n" (Lam "f" (Lam "x" 
>           (App (Var "f") 
>                (App (App (Var "n") (Var "f"))
>                     (Var "x")))))
>
> add = Lam "m" (Lam "n" (Lam "f" (Lam "x"
>           (App (App (Var "m") (Var "f"))
>                (App (App (Var "n") (Var "f"))
>                     (Var "x"))))))
>
> mul = Lam "m" (Lam "n" (Lam "f"
>           (App (Var "m") (App (Var "n") (Var "f")))))
>
> exP = Lam "m" (Lam "n" (App (Var "n") (Var "m")))

Tests:

> e3a  = App (App add num3) num4  -- 3+4 = 7
> e3b  = App (App mul num7) num6  -- 7*6 = 42
> e3c  = App (App exP num3) num4  -- 3^4 = 81
> e3d  = App isZero num0	  -- true
> e3e  = App isZero num1          -- false
> e3f  = App isZero e3b           -- false


4) Define the Y combinator using the lambda calculus interpreter, and
provide alternative definitions of ADD and MULT using Y.  To do this,
you will need a predecessor function:

PRED = lambda n. lambda s. lambda z.
                   let s2 = lambda n. lambda f. f (n s),
                       z2 = lambda f. z
                   in n s2 z2 (lambda x.x),

Test your implementation.

Y Combinator:

> y = Lam "f" (App delta delta)
> delta = Lam "x" (App (Var "f") (App (Var "x") (Var "x")))

PRED function:

> pre = let s2 = Lam "n" (Lam "f" (App (Var "f") (App (Var "n") (Var "s"))))
>           z2 = Lam "f" (Var "z")
>       in Lam "n" (Lam "s" (Lam "z"
>            (App (App (App (Var "n") s2) z2) (Lam "x" (Var "x")))))

For clarity:

> cond  = Lam "b" (Lam "c" (Lam "a" (App (App (Var "b") (Var "c")) (Var "a"))))

Recursive versions of ADD and MULT in Haskell:

> addrec n1 n2 = if n2==0 then n1
>                else addrec (n1+1) (n2-1)
> 
> mulrec n1 n2 = let loop n2 acc = if n2==0 then acc
>                                  else loop (n2-1) (acc+n1)
>                in loop n2 0

Now in LC:

> addRec = App y 
>    (Lam "add" (Lam "n1" (Lam "n2"
>         (App (App (App cond 
>                        (App isZero (Var "n2")))
>                   (Var "n1"))
>              (App (App (Var "add") 
>                        (App suc (Var "n1")))
>                   (App pre (Var "n2")))))))
>
> mulRec = Lam "n1" (Lam "n2" (App (App loop (Var "n2")) num0))
> loop = App y (Lam "loop" (Lam "n2" (Lam "acc"
>         (App (App (App cond 
>                        (App isZero (Var "n2")))
>                   (Var "acc"))
>              (App (App (Var "loop") 
>                        (App pre (Var "n2")))
>                   (App (App add (Var "acc")) (Var "n1")))))))

Tests:

> e4a = App pre num1		   -- 1-1 = 0
> e4b = App pre e3a                -- 7-1 = 6
> e4c = App (App addRec num2) num3 -- 2+3 = 5
> e4d = App (App mulRec num2) num0 -- 2*0 = 0
> e4e = App (App mulRec num2) num3 -- 2*3 = 6


5) Define lambda calculus terms PAIR, LEFT, and RIGHT with the
following properties:
 
    LEFT (PAIR X Y)  -->*  X
    RIGHT (PAIR X Y)  -->*  Y
 
Implement these in the lambda calculus interpreter and verify that
they work as described above.

> pair  = Lam "l" (Lam "r" (Lam "s" (App (App (Var "s") (Var "l")) (Var "r"))))
> left  = Lam "p" (App (Var "p") (Lam "l" (Lam "r" (Var "l"))))
> right = Lam "p" (App (Var "p") (Lam "l" (Lam "r" (Var "r"))))

> e5a = App (App pair num1) num2  -- (1,2)
> e5b = App left  e5a             -- left  (1,2) = 1
> e5c = App right e5a             -- right (1,2) = 2


6) Using the Y combinator, define an infinite sequence of ones called
ONES that is equivalent to the following recursive definition:
 
    ONES = PAIR ONE ONES
 
Then evaluate LEFT ONES using both normal-order and eager evaluation.

> ones = App y (Lam "ones" (App (App pair num1) (Var "ones")))

Tests:

> e6a = App left ones
> e6b = App left (App right ones)