From c98765240c1e760147d61a996316ad4dbed4d449 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 23 Nov 2020 14:44:15 -0800 Subject: [PATCH] Add Homework 6 --- DeBruijn.hs | 454 ++++++++++++++++++++++++++++++++++++++++++++++++++++ HW6.hs | 224 ++++++++++++++++++++++++++ 2 files changed, 678 insertions(+) create mode 100644 DeBruijn.hs create mode 100644 HW6.hs diff --git a/DeBruijn.hs b/DeBruijn.hs new file mode 100644 index 0000000..58b2e9e --- /dev/null +++ b/DeBruijn.hs @@ -0,0 +1,454 @@ +-- | This module illustrates beta-reduction on nameless lambda calculus +-- terms using de Bruijn indexes. +module DeBruijn where + +import Prelude hiding (print,and,or,not,pred,succ,fst,snd,either,length,sum,product) + + +-- +-- * Syntax +-- + +-- ** Abstract syntax + +-- | The de Bruijn index of a variable. +type Var = Int + +-- | Nameless lambda calculus terms. Note that we can check alpha-equivalence +-- with plain old Haskell (==). This is a more complicated and expensive +-- operation in named lambda calculuses. +data Exp + = Ref Var -- ^ variable reference + | App Exp Exp -- ^ application + | Abs Exp -- ^ lambda abstraction + deriving (Eq,Show) + + +-- ** Syntactic sugar + +-- | Build an abstraction that takes two arguments. +abs2 :: Exp -> Exp +abs2 = Abs . Abs + +-- | Build an abstraction that takes three arguments. +abs3 :: Exp -> Exp +abs3 = abs2 . Abs + +-- | Build an abstraction that takes four arguments. +abs4 :: Exp -> Exp +abs4 = abs3 . Abs + +-- | Build an application to apply a function to two arguments. +app2 :: Exp -> Exp -> Exp -> Exp +app2 f e1 e2 = App (App f e1) e2 + +-- | Build an application to apply a function to three arguments. +app3 :: Exp -> Exp -> Exp -> Exp -> Exp +app3 f e1 e2 e3 = App (app2 f e1 e2) e3 + +-- | Build an application to apply a function to four arguments. +app4 :: Exp -> Exp -> Exp -> Exp -> Exp -> Exp +app4 f e1 e2 e3 e4 = App (app3 f e1 e2 e3) e4 + + +-- ** Pretty printing + +-- | Pretty print a nameless lambda calculus expression. +pretty :: Exp -> String +pretty e = case e of + Ref x -> show x + Abs e -> "λ" ++ pretty e + App l r -> inAppL l ++ " " ++ group r + where + group (Ref x) = show x + group e = "(" ++ pretty e ++ ")" + inAppL (App l r) = inAppL l ++ " " ++ group r + inAppL e = group e + +-- | Print a pretty-printed lambda calculus expression to standard output. +print :: Exp -> IO () +print = putStrLn . pretty + + +-- +-- * Semantics +-- + +-- ** Substitution + +-- | Variable substitution. `sub x arg e` substitues arg for every x in e. +-- +-- Both the abstraction and reference cases are interesting. +-- +-- Each time we enter a new abstraction in e, we must: +-- 1. Increment the x that we're looking for. +-- 2. Increment all of the free variables in arg since now the references +-- will have to skip over one more lambda to get to the lambda they +-- refer to. +-- +-- For each variable reference y in e, there are three possibilities: +-- 1. It's the variable x we're looking for, in which case we replace it. +-- 2. It's a variable bound in e (y < x), in which case we do nothing. +-- 3. It's a variable that is free in e (y > x), in which case we +-- decrement it since now the reference has to skip over one less +-- lambda (i.e. the lambda that we beta-reduced away) to get to the +-- lambda it refers to. +-- +-- >>> sub 0 (Ref 1) (Abs (Ref 1)) +-- Abs (Ref 2) +-- +sub :: Var -> Exp -> Exp -> Exp +sub x arg (App l r) = App (sub x arg l) (sub x arg r) +sub x arg (Abs e) = Abs (sub (x+1) (inc 0 arg) e) +sub x arg (Ref y) + | y == x = arg -- found an x, replace it! + | y < x = Ref y -- not x and bound in e, leave it alone + | y > x = Ref (y-1) -- not x and free in e, decrement it + +-- | Increment the free variables in an expression. +-- +-- The argument d (for "depth") indicates the number of abstractions we +-- have recursed into so far. A variable that is smaller than the depth +-- is not free, and so should not be incremented. +-- +-- >>> inc 0 (Ref 0) +-- Ref 1 +-- +-- >>> inc 0 (App (Ref 1) (Abs (Ref 0))) +-- App (Ref 2) (Abs (Ref 0)) +-- +inc :: Int -> Exp -> Exp +inc d (App l r) = App (inc d l) (inc d r) +inc d (Abs e) = Abs (inc (d+1) e) +inc d (Ref x) = Ref (if x < d then x else x+1) + + +-- ** Small-step semantics + +-- | Do one step of normal order reduction and return the result. +-- If no redex is found, return Nothing. +-- +-- The first case matches a redex and does a substitution. The rest of +-- the cases implement a search for next redex. +-- +-- >>> step (App (Abs (Ref 0)) (Ref 1)) +-- Just (Ref 1) +-- +-- >>> step (App (abs2 (App (Ref 0) (Ref 1))) (Ref 2)) +-- Just (Abs (App (Ref 0) (Ref 3))) +-- +-- >>> step (App (abs2 (App (Ref 2) (Ref 1))) (Ref 0)) +-- Just (Abs (App (Ref 1) (Ref 1))) +-- +step :: Exp -> Maybe Exp +step (App (Abs e) r) = Just (sub 0 r e) -- found a redex, do beta reduction! +step (App l r) = case step l of + Just l' -> Just (App l' r) + Nothing -> fmap (App l) (step r) +step (Abs e) = fmap Abs (step e) +step (Ref _) = Nothing + + +-- | Evaluate an expression to normal form using normal order recution. +-- Return a list of expressions produced by each step of reduction. +-- Note that this list may be infinite if the reduction never reaches +-- a normal form! +steps :: Exp -> [Exp] +steps e = e : case step e of + Nothing -> [] + Just e' -> steps e' + +-- | Evaluate an expression to normal form using normal order reduction. +-- Note that this function will not terminate if the reduction never +-- reaches a normal form! +eval :: Exp -> Exp +eval = last . steps + +-- | Print a reduction sequence for an expression. +printReduce :: Exp -> IO () +printReduce = mapM_ print . steps + + +-- +-- * Church encodings +-- + +-- ** Church booleans + +-- | λxy.x +true :: Exp +true = abs2 (Ref 1) + +-- | λxy.y +false :: Exp +false = abs2 (Ref 0) + +-- | λbte.bte +if_ :: Exp +if_ = abs3 (app2 (Ref 2) (Ref 1) (Ref 0)) + +-- | λb. if b false true +not :: Exp +not = Abs (app3 if_ (Ref 0) false true) + +-- | λpq. if p q p +and :: Exp +and = abs2 (app3 if_ (Ref 1) (Ref 0) (Ref 1)) + +-- | λpq. if p p q +or :: Exp +or = abs2 (app3 if_ (Ref 1) (Ref 1) (Ref 0)) + +-- | Church Boolean tests: +-- +-- >>> true == eval (app2 and (app2 or false true) (App not false)) +-- True +-- +-- >>> false == eval (app2 or (App not true) (app2 and true false)) +-- True + + +-- ** Church numerals + +-- | λfx.x +zero :: Exp +zero = abs2 (Ref 0) + +-- | λfx.fx +one :: Exp +one = abs2 (App (Ref 1) (Ref 0)) + +-- | λfx.f(fx) +two :: Exp +two = abs2 (App (Ref 1) (App (Ref 1) (Ref 0))) + +-- | λfx.f(f(fx)) +three :: Exp +three = abs2 (App (Ref 1) (App (Ref 1) (App (Ref 1) (Ref 0)))) + +-- | Build a Church numeral for an arbitrary natural number. +-- +-- >>> map num [0,1,2,3] == [zero,one,two,three] +-- True +-- +num :: Int -> Exp +num n = abs2 (help n (Ref 0)) + where help 0 e = e + help n e = App (Ref 1) (help (n-1) e) + +-- | λnfx.f(nfx) +succ :: Exp +succ = abs3 (App (Ref 1) (app2 (Ref 2) (Ref 1) (Ref 0))) + +-- | λnmfx.nf(mfx) +add :: Exp +add = abs4 (app2 (Ref 3) (Ref 1) (app2 (Ref 2) (Ref 1) (Ref 0))) + +-- | λnmf.n(mf) +mult :: Exp +mult = abs3 (App (Ref 2) (App (Ref 1) (Ref 0))) + +-- | λn. n (λx.false) true +isZero :: Exp +isZero = Abs (app2 (Ref 0) (Abs false) true) + +-- | λnfx.n (λgh.h(gf)) (λu.x) (λu.u) +-- +-- See: https://en.wikipedia.org/wiki/Church_encoding#Derivation_of_predecessor_function +pred :: Exp +pred = abs3 (app3 (Ref 2) + (abs2 (App (Ref 0) (App (Ref 1) (Ref 3)))) + (Abs (Ref 1)) + (Abs (Ref 0))) + +-- | Church numeral tests: +-- +-- >>> three == eval (app2 add two one) +-- True +-- +-- >>> num 15 == eval (app2 mult (app2 add two three) three) +-- True +-- +-- >>> num 5 == eval (App pred (num 6)) +-- True + + +-- ** Church tuples + +-- | λxys.sxy +-- +-- >>> two == eval (App fst (app2 pair two true)) +-- True +-- +-- >>> true == eval (App snd (app2 pair two true)) +-- True +-- +pair :: Exp +pair = abs3 (app2 (Ref 0) (Ref 2) (Ref 1)) + +-- | λt.t(λxy.x) +fst :: Exp +fst = Abs (App (Ref 0) true) + +-- | λt.t(λxy.y) +snd :: Exp +snd = Abs (App (Ref 0) false) + +-- | λxyzs.sxyz +-- +-- >>> one == eval (App sel13 (app3 tuple3 one two three)) +-- True +-- +-- >>> two == eval (App sel23 (app3 tuple3 one two three)) +-- True +-- +-- >>> three == eval (App sel33 (app3 tuple3 one two three)) +-- True +-- +tuple3 :: Exp +tuple3 = abs4 (app3 (Ref 0) (Ref 3) (Ref 2) (Ref 1)) + +-- | λt.t(λxyz.x) +sel13 :: Exp +sel13 = Abs (App (Ref 0) (abs3 (Ref 2))) + +-- | λt.t(λxyz.y) +sel23 :: Exp +sel23 = Abs (App (Ref 0) (abs3 (Ref 1))) + +-- | λt.t(λxyz.z) +sel33 :: Exp +sel33 = Abs (App (Ref 0) (abs3 (Ref 0))) + + +-- ** Church sums + +-- | λfgu.ufg +-- +-- >>> three == eval (app3 either succ not (App inL two)) +-- True +-- +-- >>> false == eval (app3 either succ not (App inR true)) +-- True +-- +either :: Exp +either = pair + +-- | λxfg.fx +inL :: Exp +inL = abs3 (App (Ref 1) (Ref 2)) + +-- | λxfg.gx +inR :: Exp +inR = abs3 (App (Ref 0) (Ref 2)) + +-- | λfghu.ufgh +-- +-- >>> three == eval (app4 case3 succ not fst (App in13 two)) +-- True +-- +-- >>> false == eval (app4 case3 succ not fst (App in23 true)) +-- True +-- +-- >>> one == eval (app4 case3 succ not fst (App in33 (app2 pair one two))) +-- True +-- +case3 :: Exp +case3 = tuple3 + +-- | λxfgh.fx +in13 :: Exp +in13 = abs4 (App (Ref 2) (Ref 3)) + +-- | λxfgh.gx +in23 :: Exp +in23 = abs4 (App (Ref 1) (Ref 3)) + +-- | λxfgh.hx +in33 :: Exp +in33 = abs4 (App (Ref 0) (Ref 3)) + + +-- ** Fixpoint combinator + +-- | λf. (λx.f(xx)) (λx.f(xx)) +fix :: Exp +fix = Abs (App (Abs (App (Ref 1) (App (Ref 0) (Ref 0)))) + (Abs (App (Ref 1) (App (Ref 0) (Ref 0))))) + +-- | fix (λrn. if (isZero n) one (mult n (r (pred n)))) +-- +-- >>> num 6 == eval (App fac three) +-- True +-- +-- >>> num 24 == eval (App fac (num 4)) +-- True +-- +fac :: Exp +fac = App fix (abs2 + (app3 if_ + (App isZero (Ref 0)) -- condition + one -- base case + (app2 mult -- recursive case + (Ref 0) + (App (Ref 1) (App pred (Ref 0)))))) + + +-- ** Church-encoded lists + +-- | inL (λx.x) +nil :: Exp +nil = App inL (Abs (Ref 0)) + +-- | λht. inR (pair h t) +cons :: Exp +cons = abs2 (App inR (app2 pair (Ref 1) (Ref 0))) + +-- | fix (λrfbl. either (λx.b) (λp. f (fst p) (r f b (snd p))) l) +fold :: Exp +fold = App fix (abs4 + (app3 either + (Abs (Ref 2)) + (Abs (app2 (Ref 3) + (App fst (Ref 0)) + (app3 (Ref 4) (Ref 3) (Ref 2) (App snd (Ref 0))))) + (Ref 0))) + +-- | Smart constructor to build a Church-encoded list of natural numbers. +list :: [Int] -> Exp +list = foldr (app2 cons . num) nil + +-- | fold (λh. add one) zero +-- +-- >>> three == eval (App length (list [2,3,4])) +-- True +-- +length :: Exp +length = app2 fold (Abs (App add one)) zero + +-- | fold add zero +-- +-- >>> num 9 == eval (App sum (list [2,3,4])) +-- True +-- +-- >>> num 55 == eval (App sum (list [1..10])) +-- True +-- +sum :: Exp +sum = app2 fold add zero + +-- | fold mult one +-- +-- >>> num 24 == eval (App product (list [2,3,4])) +-- True +-- +product :: Exp +product = app2 fold mult one + +-- | λf. fold (\h. cons (f h)) nil +-- +-- >>> eval (list [4,5,6]) == eval (app2 map' (App add two) (list [2,3,4])) +-- True +-- +map' :: Exp +map' = Abs (app2 fold (Abs (App cons (App (Ref 1) (Ref 0)))) nil) diff --git a/HW6.hs b/HW6.hs new file mode 100644 index 0000000..f67a835 --- /dev/null +++ b/HW6.hs @@ -0,0 +1,224 @@ +module HW6 where + +import Prelude hiding (print,and,or,not,pred,succ,fst,snd,either,length,sum,product) + +import DeBruijn + + +-- +-- * Part 1: Nameless lambda calculus +-- + +-- | λx. (λx.x) x +-- +-- >>> eval ex1 +-- Abs (Ref 0) +-- +ex1 :: Exp +ex1 = Abs (App (Abs (Ref 0)) (Ref 0)) + +-- | (λxy.xz) z z +-- +-- >>> eval ex2 +-- App (Ref 0) (Ref 0) +-- +ex2 :: Exp +ex2 = App (App (Abs (Abs (App (Ref 1) (Ref 2)))) (Ref 0)) (Ref 0) + +-- | λy. (λxy.yx) y z +-- +-- >>> eval ex3 +-- Abs (App (Ref 1) (Ref 0)) +-- +ex3 :: Exp +ex3 = Abs (App (App (Abs (Abs (App (Ref 0) (Ref 1)))) (Ref 0)) (Ref 1)) + + +-- | Is the given nameless lambda calculus term a closed expression? That is, +-- does it contain no free variables? +-- +-- >>> closed (Ref 0) +-- False +-- +-- >>> closed (Abs (Ref 0)) +-- True +-- +-- >>> closed (Abs (App (Ref 0) (Ref 1))) +-- False +-- +-- >>> closed (Abs (App (Abs (App (Ref 0) (Ref 1))) (Ref 0))) +-- True +-- +closed :: Exp -> Bool +closed = cl 0 + where + cl n (Ref i) = i < n + cl n (App l r) = cl n l && cl n r + cl n (Abs e) = cl (n+1) e + + +-- +-- * Part 2: Church pair update functions +-- + +-- | Write a lambda calculus function that replaces the first element in a +-- Church-encoded pair. The first argument to the function is the new +-- first element, the second argument is the original pair. +-- +-- >>> :{ +-- eval (app2 pair true (num 3)) == +-- eval (app2 setFst true (app2 pair (num 2) (num 3))) +-- :} +-- True +-- +setFst :: Exp +setFst = Abs $ Abs $ Abs $ App (Ref 1) (Abs $ Abs $ App (App (Ref 2) (Ref 4)) (Ref 0)) + -- \x -> \p -> \f -> p (\a -> \b -> f x b) + +-- | Write a lambda calculus function that replaces the second element in a +-- Church-encoded pair. The first argument to the function is the new +-- second element, the second argument is the original pair. +-- +-- >>> :{ +-- eval (app2 pair (num 2) true) == +-- eval (app2 setSnd true (app2 pair (num 2) (num 3))) +-- :} +-- True +-- +setSnd :: Exp +setSnd = Abs $ Abs $ Abs $ App (Ref 1) (Abs $ Abs $ App (App (Ref 2) (Ref 1)) (Ref 4)) + -- \x -> \p -> \f -> p (\a -> \b -> f a x) + +-- +-- * Part 3: Church encoding a Haskell program +-- + +-- | Pretend Haskell's Int is restricted to Nats. +type Nat = Int + +-- | A simple data for representing shapes. +data Shape + = Circle Nat + | Rectangle Nat Nat + deriving (Eq,Show) + +-- | A smart constructor for building squares. +square :: Nat -> Shape +square l = Rectangle l l + +-- | Compute the area of a shape using a rough approximation of pi. +area :: Shape -> Nat +area (Circle r) = 3 * r * r +area (Rectangle l w) = l * w + +-- | Compute the perimeter of a shape using a rough approximation of pi. +perimeter :: Shape -> Nat +perimeter (Circle r) = 2 * 3 * r +perimeter (Rectangle l w) = 2 * l + 2 * w + +-- | Encode the circle constructor as a lambda calculus term. The term +-- should be a function that takes a Church-encoded natural number as input +-- and produces a Church-encoded shape as output. +circleExp :: Exp +circleExp = inL + +-- | Encode the rectangle constructor as a lambda calculus term. The term +-- should be a function that takes two Church-encoded natural numbers as +-- input and produces a Church-encoded shape as output. +rectangleExp :: Exp +rectangleExp = Abs $ Abs $ App inR $ app2 pair (Ref 1) (Ref 0) + +-- | Convert a shape into a lambda calculus term. This function helps to +-- illustrate how your encodings of the constructors should work. +encodeShape :: Shape -> Exp +encodeShape (Circle r) = App circleExp (num r) +encodeShape (Rectangle l w) = app2 rectangleExp (num l) (num w) + +-- | Encode the square function as a lambda calculus term. +squareExp :: Exp +squareExp = Abs $ app2 rectangleExp (Ref 0) (Ref 0) + +-- | Encode the area function as a lambda calculus term. +areaExp :: Exp +areaExp = Abs $ app2 (Ref 0) + (Abs $ app2 mult (num 3) (app2 mult (Ref 0) (Ref 0))) + (Abs $ App (Ref 0) mult) + +-- | Encode the perimeter function as a lambda calculus term. +perimeterExp :: Exp +perimeterExp = Abs $ app2 (Ref 0) + (Abs $ app2 mult (num 6) (Ref 0)) + (Abs $ App (Ref 0) $ Abs $ Abs $ app2 mult (num 2) (app2 add (Ref 0) (Ref 1))) + +-- | Some tests of your lambda calculus encodings. +-- +-- >>> :{ +-- checkEval (area (Circle 3)) +-- (App areaExp (App circleExp (num 3))) +-- :} +-- True +-- +-- >>> :{ +-- checkEval (area (Rectangle 3 5)) +-- (App areaExp (app2 rectangleExp (num 3) (num 5))) +-- :} +-- True +-- +-- >>> :{ +-- checkEval (area (square 4)) +-- (App areaExp (App squareExp (num 4))) +-- :} +-- True +-- +-- >>> :{ +-- checkEval (perimeter (Circle 3)) +-- (App perimeterExp (App circleExp (num 3))) +-- :} +-- True +-- +-- >>> :{ +-- checkEval (perimeter (Rectangle 3 5)) +-- (App perimeterExp (app2 rectangleExp (num 3) (num 5))) +-- :} +-- True +-- +-- >>> :{ +-- checkEval (perimeter (square 4)) +-- (App perimeterExp (App squareExp (num 4))) +-- :} +-- True +-- +checkEval :: Nat -> Exp -> Bool +checkEval n e = num n == eval e + +-- Alright, extra practice, let's go. +-- Part 1: 4-tuples (Bonus: n-tuples) +absN :: Int -> Exp -> Exp +absN n = flip (foldr $ const Abs) $ replicate n () + +apps :: Exp -> [Exp] -> Exp +apps e = foldl App e + +tupleN :: Int -> Exp +tupleN n = absN (n+1) $ apps (Ref 0) $ map Ref $ [n, (n-1) .. 1] + +selN :: Int -> Int -> Exp +selN n m = Abs $ App (Ref 0) $ absN m $ Ref $ m - n + +tuple4 :: Exp +tuple4 = tupleN 4 + +sel14 :: Exp +sel14 = selN 1 4 + +sel24 :: Exp +sel24 = selN 2 4 + +sel34 :: Exp +sel34 = selN 3 4 + +sel44 :: Exp +sel44 = selN 4 4 + +-- Wait, the extra credit practice is mostly mechanical? +-- Boo!