Added nullary applications and generalized eta reductions.
parent
2e95783c3a
commit
5f87100363
32
README.md
32
README.md
|
@ -13,7 +13,35 @@ Exit the prompt with `Ctrl-C` (or however else you kill a program in your termin
|
|||
|
||||
Bound variables will be printed followed by a number representing the number of binders
|
||||
between it and its definition for disambiguation.
|
||||
This is not guaranteed not to capture free variables.
|
||||
|
||||
## Differences from the traditional lambda calculus
|
||||
This version of the lambda calculus is completely compatible
|
||||
with the traditional lambda calculus, but features a few extensions.
|
||||
|
||||
### Nullary applications
|
||||
In any binary application `(f x)`, the `f` is a function and the `x` is a variable.
|
||||
Applications are left-associative, meaning `(f x y)` equals `((f x) y)`.
|
||||
Any term `x` may be expanded to an application `(id x)`.
|
||||
Working backwards, we have `(f x y)` equals `(((id f) x) y)`.
|
||||
Thus we may reasonably say that `() = id`
|
||||
and thus that `(f x y)` equals `(((() f) x) y)`,
|
||||
and that `(x)` equals `(() x)`, which reduces to just `x`.
|
||||
|
||||
### Nullary functions and generalized eta reductions
|
||||
We can apply a similar argument to the function syntax.
|
||||
`(\x y z. E)` is the same as `(\x.(\y.(\z.E)))` because lambda is right-associative.
|
||||
Any term `x` may be eta-expanded into a lambda `(\y. ((() x) y))`.
|
||||
Working backwards, we have `(\x. (() x))` eta-reducing to `()`.
|
||||
Therefore, the identity function eta-reduces to just `()`.
|
||||
|
||||
Again similarly we have the nulladic lambda syntax `(\.E)`
|
||||
which trivially beta-reduces to `E`.
|
||||
|
||||
I also take any series of ordered applications
|
||||
`(\v v1 v2 ... vn. v:n v2:(n-1) ... v(n-1):1 vn:0)`
|
||||
to eta-reduce to `()` (including `()` itself and, trivially, `(\x. x)`).
|
||||
|
||||
### Nullary functions
|
||||
|
||||
### Examples
|
||||
```
|
||||
|
@ -28,7 +56,7 @@ y
|
|||
## Syntax
|
||||
* Variables are alphanumeric, beginning with a letter.
|
||||
* Applications are left-associative, and parentheses are not necessary.
|
||||
* Lambdas are represented by `\\`, bind as far right as possible, and parentheses are not necessary.
|
||||
* Lambdas are represented by `\`, bind as far right as possible, and parentheses are not necessary.
|
||||
|
||||
### Examples
|
||||
* Variables: `x`, `abc`, `D`, `fooBar`, `f10`
|
||||
|
|
|
@ -1,11 +1,12 @@
|
|||
{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, MultiWayIf #-}
|
||||
module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), ReaderAlg, eval, cataReader) where
|
||||
module UntypedLambdaCalculus (Expr (Free, Var, Lam, App, Nil), ReaderAlg, eval, cataReader) where
|
||||
|
||||
import Control.Monad.Reader (Reader, runReader, local, reader, ask)
|
||||
import Data.Bifunctor (bimap)
|
||||
import Data.Foldable (fold)
|
||||
import Data.Functor ((<&>))
|
||||
import Data.Functor.Foldable (Base, Recursive, cata)
|
||||
import Data.Functor.Foldable (Base, Recursive, cata, embed, project)
|
||||
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
||||
import Data.Monoid (Any (Any, getAny))
|
||||
|
||||
-- | A lambda calculus expression where variables are identified
|
||||
-- | by their distance from their binding site (De Bruijn indices).
|
||||
|
@ -13,6 +14,7 @@ data Expr = Free String
|
|||
| Var Int
|
||||
| Lam String Expr
|
||||
| App Expr Expr
|
||||
| Nil
|
||||
|
||||
makeBaseFunctor ''Expr
|
||||
|
||||
|
@ -25,55 +27,75 @@ cataReader f initialState x = runReader (cata f x) initialState
|
|||
instance Show Expr where
|
||||
show = cataReader alg []
|
||||
where alg :: ReaderAlg ExprF [String] String
|
||||
alg (FreeF v) = return v
|
||||
alg (VarF v) = reader (\vars -> vars !! v ++ ':' : show v)
|
||||
alg (LamF v e) = do
|
||||
alg (FreeF v) = return v
|
||||
alg (VarF i) = reader (\vars -> vars !! i ++ ':' : show i)
|
||||
alg (LamF v e) = do
|
||||
body <- local (v :) e
|
||||
return $ "(\\" ++ v ++ ". " ++ body ++ ")"
|
||||
alg (AppF f' x') = do
|
||||
f <- f'
|
||||
x <- x'
|
||||
return $ "(" ++ f ++ " " ++ x ++ ")"
|
||||
alg NilF = return "()"
|
||||
|
||||
-- | Determine whether the variable bound by a lambda expression is used in its body.
|
||||
-- | This is used in eta reduction, where `(\x. f x)` reduces to `f` when `x` is not bound in `f`.
|
||||
-- | Is the innermost bound variable of this subexpression (`Var 0`) used in its body?
|
||||
-- | For example: in `\x. a:1 x:0 b:2`, `x:0` is bound in `a:1 x:0 b:2`.
|
||||
-- | On the other hand, in `\x. a:3 b:2 c:1`, it is not.
|
||||
bound :: Expr -> Bool
|
||||
bound = getAny . cataReader alg 0
|
||||
where alg :: ReaderAlg ExprF Int Any
|
||||
alg (VarF index) = reader (Any . (== index))
|
||||
alg (LamF _ e) = local (+ 1) e
|
||||
alg x = fold <$> sequenceA x
|
||||
|
||||
-- | Opposite of `bound`.
|
||||
unbound :: Expr -> Bool
|
||||
unbound = cataReader alg 0
|
||||
where alg :: ReaderAlg ExprF Int Bool
|
||||
alg (FreeF _) = return True
|
||||
alg (VarF v) = reader (/= v)
|
||||
alg (AppF f x) = (&&) <$> f <*> x
|
||||
alg (LamF _ e) = local (+ 1) e
|
||||
unbound = not . bound
|
||||
|
||||
-- | When we bind a new variable, we enter a new scope.
|
||||
-- | Since variables are identified by their distance from their binder,
|
||||
-- | we must increment them to account for the incremented distance,
|
||||
-- | thus embedding them into the new expression.
|
||||
embed :: Expr -> Expr
|
||||
embed (Var v) = Var $ v + 1
|
||||
embed (App f x) = App (embed f) (embed x)
|
||||
embed x = x
|
||||
liftExpr :: Int -> Expr -> Expr
|
||||
liftExpr n (Var i) = Var $ i + n
|
||||
liftExpr _ o@(Lam _ _) = o
|
||||
liftExpr n x = embed $ fmap (liftExpr n) $ project x
|
||||
|
||||
subst :: Expr -> Expr -> Expr
|
||||
subst val = cataReader alg (0, val)
|
||||
where alg :: ReaderAlg ExprF (Int, Expr) Expr
|
||||
alg (FreeF x) = return $ Free x
|
||||
alg (VarF x) = ask <&> \(x', value) -> if
|
||||
| x == x' -> value
|
||||
| x > x' -> Var $ x - 1
|
||||
| otherwise -> Var x
|
||||
alg (AppF f x) = App <$> f <*> x
|
||||
alg (LamF v e) = Lam v <$> local (bimap (+ 1) embed) e
|
||||
subst val = cataReader alg 0
|
||||
where alg :: ReaderAlg ExprF Int Expr
|
||||
alg (VarF i) = ask <&> \bindingDepth -> if
|
||||
| i == bindingDepth -> liftExpr bindingDepth val
|
||||
| i > bindingDepth -> Var $ i - 1
|
||||
| otherwise -> Var i
|
||||
alg (LamF v e) = Lam v <$> local (+ 1) e
|
||||
alg x = embed <$> sequence x
|
||||
|
||||
-- | Generalized eta reduction. I (almost certainly re-)invented it myself.
|
||||
etaReduce :: Expr -> Expr
|
||||
-- Degenerate case
|
||||
-- The identity function reduces to the syntactic identity, `Nil`.
|
||||
etaReduce (Lam _ (Var 0)) = Nil
|
||||
-- `\x. f x -> f` if `x` is not bound in `f`.
|
||||
etaReduce o@(Lam _ (App f (Var 0)))
|
||||
| unbound f = eval $ subst undefined f
|
||||
| otherwise = o
|
||||
-- `\x y. f y -> \x. f` if `y` is not bound in `f`;
|
||||
-- the resultant term may itself be eta-reducible.
|
||||
etaReduce (Lam v e'@(Lam _ _)) = case etaReduce e' of
|
||||
e@(Lam _ _) -> Lam v e
|
||||
e -> etaReduce $ Lam v e
|
||||
etaReduce x = x
|
||||
|
||||
betaReduce :: Expr -> Expr
|
||||
betaReduce (App f' x) = case eval f' of
|
||||
Lam _ e -> eval $ subst x e
|
||||
Nil -> eval x
|
||||
f -> App f $ eval x
|
||||
betaReduce x = x
|
||||
|
||||
-- | Evaluate an expression to normal form.
|
||||
eval :: Expr -> Expr
|
||||
eval (App f' x) = case eval f' of
|
||||
-- Beta reduction.
|
||||
Lam _ e -> eval $ subst x e
|
||||
f -> App f (eval x)
|
||||
eval o@(Lam _ (App f (Var 0)))
|
||||
-- Eta reduction. We know that `0` is not bound in `f`,
|
||||
-- so we can simply substitute it for undefined.
|
||||
| unbound f = eval $ subst undefined f
|
||||
| otherwise = o
|
||||
eval a@(App _ _) = betaReduce a
|
||||
eval l@(Lam _ _) = etaReduce l
|
||||
eval o = o
|
||||
|
|
|
@ -3,15 +3,15 @@ module UntypedLambdaCalculus.Parser (parseExpr) where
|
|||
|
||||
import Control.Applicative (liftA2)
|
||||
import Control.Monad.Reader (local, asks)
|
||||
import Data.List (foldl1', elemIndex)
|
||||
import Data.List (foldl', elemIndex)
|
||||
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
||||
import Text.Parsec (SourceName, ParseError, (<|>), many, sepBy1, letter, alphaNum, char, between, spaces, parse)
|
||||
import Text.Parsec (SourceName, ParseError, (<|>), many, sepBy, letter, alphaNum, char, between, spaces, parse)
|
||||
import Text.Parsec.String (Parser)
|
||||
import UntypedLambdaCalculus (Expr (Free, Var, Lam, App), ReaderAlg, cataReader)
|
||||
import UntypedLambdaCalculus (Expr (Free, Var, Lam, App, Nil), ReaderAlg, cataReader)
|
||||
|
||||
data Ast = AstVar String
|
||||
| AstLam String Ast
|
||||
| AstApp Ast Ast
|
||||
| AstLam [String] Ast
|
||||
| AstApp [Ast]
|
||||
|
||||
makeBaseFunctor ''Ast
|
||||
|
||||
|
@ -30,14 +30,14 @@ parens = between (char '(') (char ')')
|
|||
-- | A lambda expression.
|
||||
lam :: Parser Ast
|
||||
lam = do
|
||||
vars <- between (char '\\') (char '.') $ name `sepBy1` spaces
|
||||
vars <- between (char '\\') (char '.') $ name `sepBy` spaces
|
||||
spaces
|
||||
body <- app
|
||||
return $ foldr AstLam body vars
|
||||
return $ AstLam vars body
|
||||
|
||||
-- | An application expression.
|
||||
app :: Parser Ast
|
||||
app = foldl1' AstApp <$> safeExpr `sepBy1` spaces
|
||||
app = AstApp <$> safeExpr `sepBy` spaces
|
||||
|
||||
-- | An expression, but where applications must be surrounded by parentheses,
|
||||
-- | to avoid ambiguity (infinite recursion on `app` in the case where the first
|
||||
|
@ -54,8 +54,9 @@ toExpr = cataReader alg []
|
|||
return $ case bindingSite of
|
||||
Just index -> Var index
|
||||
Nothing -> Free varName
|
||||
alg (AstLamF varName body) = Lam varName <$> local (varName :) body
|
||||
alg (AstAppF f x) = App <$> f <*>x
|
||||
alg (AstLamF vars body) = foldr (\v e -> Lam v <$> local (v :) e) body vars
|
||||
alg (AstAppF [e]) = e
|
||||
alg (AstAppF es) = foldl' App Nil <$> sequenceA es
|
||||
|
||||
-- | Since applications do not require parentheses and can contain only a single item,
|
||||
-- | the `app` parser is sufficient to parse any expression at all.
|
||||
|
|
Loading…
Reference in New Issue