Code and Notes (Week 3 Thursday)
Table of Contents
1. Church Encodings of Booleans and Naturals
-- Church encoding of Boolean terms type Church_Bool a = a -> a -> a true :: Church_Bool a true = (\a b -> a) false = (\a b -> b) -- similar to the slides conj = (\p q -> p q false) -- does conj true false β-reduce to anything interesting? -- let's use conj == (\p q -> p q p) -- conj true false == (\p q -> p q )(\a b -> a)(\a b -> b) -- β== (\q -> (\a b -> a) q (\a b -> a))(\a b -> b) by β-reducing p := \a b -> a -- β== (\q -> (\b -> q) (\a b -> a))(\a b -> b) β-reducing a := q -- β== (\q -> q)(\a b -> b) β-reducing b := \a b -> a -- β== (\a b -> b) β-reducing q := \a b -> b -- To provide the type of booleans to some client, we need to provide a -- True constant, a False constant, and a way to perform a case-division, -- which we can encode into a case constant. The Church encoding for -- Booleans turns them into their case constant. data Bool2 = True2 | False2 x :: Bool2 x = True2 case_function_Bool2 :: Bool2 -> a -> a -> a case_function_Bool2 x true_case false_case = case x of True2 -> true_case False2 -> false_case y :: Int y = case x of True2 -> 1 False2 -> 1 -- The classic Church encoding for naturals doesn't -- work by providing a case-split, -- it provides a repetition encoder. zero = (\f x -> x) one = (\f x -> f x) two = (\f x -> f (f x)) test_church = [zero (+ 1) 0, one (+ 1) 0, two (+ 1) 0] succ = (\n f x -> f (n f x)) -- β-reducing succ one -- succ one == (\n f x -> f (n f x))(\f x -> f x) -- β== (\f x -> f ((\f x -> f x) f x)) -- β== (\f x -> f (\(x -> f x) x)) -- β== (\f x -> f (f x)
2. Elaboration on the Big-Step to Small-Step proof
A small-step semantics gives us more detail than a big-step semantics, which in turn is more detail than a denotational semantics. For our arithmetic expressions, which always evaluate to a given value, it would be easier to just use the denotational approach, the simplest approach.
We did not go into much detail about the big-step to small-step proof. This needs to construct a small-step trace for each completed big-step evaluation.
I said that this proof requires quite a bit of induction. For instance, for the case associated with a Plus construct, we have this big-step rule:
e1 ↓ v1 e2 ↓ v2 -------------------------- Plus e1 e2 ↓ (v1 + v2)
The two IHs will be that the inner evaluations have small-step traces. The completed trace for Plus will reduce first e1 then e2 to numbers (by replaying the traces from the IHs) and then reduce Plus (Num v1) (Num v2) to Num (v1 + v2) by using the final small-step rule for plus.
However, to replay the trace of steps that evaluate e1, each one needs to be lifted into a rule about Plus e1 e2 using the contextual rule. This can be animated, to some degree, by adjusting the Haskell code from Tuesday to trace not just small-steps but the justification for them.
Haskell code that does that is pretty easy to write:
small_step2 :: Arith -> Maybe (Arith, String) small_step2 (Num i) = Nothing small_step2 (Plus (Num i) (Num j)) = Just (Num (i + j), "plus main rule") small_step2 (Plus (Num i) e2) = case small_step2 e2 of Just (e2', s) -> Just (Plus (Num i) e2', "plus right-context rule of " ++ s) Nothing -> Nothing small_step2 (Plus e1 e2) = case small_step2 e1 of Just (e1', s) -> Just (Plus e1' e2, "plus left-context rule of " ++ s) Nothing -> Nothing small_step2 (Let nm (Num i) e2) = Just (subst nm (Num i) e2, "let subst") small_step2 (Let nm e1 e2) = case small_step2 e1 of Just (e1', s) -> Just (Let nm e1' e2, "let context rule of " ++ s) Nothing -> Nothing small_step2 (Var x) = error ("small_step2: encountered var " ++ x) small_steps2 (Num i) = [(Num i, "finished", Num i)] small_steps2 e = case small_step2 e of Nothing -> error ("couldn't step: " ++ show e) Just (e2, s) -> (e, s, e2) : small_steps2 e2
The formatting here is a bit ugly, but it maybe gives some idea what is going on. With some more work, we could have the Haskell code format a LaTeX script that prints inference trees for each small-step, and fills books with detailed derivations.