| Safe Haskell | Safe-Inferred |
|---|
Lessons.Lesson14
Description
Notes taken by Jonas Grybė
VARIABLE BINDING PROBLEM: When substituting in lambda calculus, we must change only FREE variables, not BOUND ones. Example: (λx.λy.x(xy)) - x and y are bound, we can't just replace them.
TWO SOLUTIONS: 1. Barendregt Convention: All variables must be unique (eliminates name conflicts). 2. De Bruijn Indices: Don't use names - use numbers indicating distance to binding lambda. Examples: λx.x → λ.0 | λx.λy.x(xy) → λ.λ.1(10) | λx.λy.b(yx) → λ.λ.2(01)
EVALUATION STRATEGIES: - Full Beta Reduction: Reduce anywhere (messy, can use function or argument first) - Call by Value: Evaluate arguments before passing (Java, C#, C) - Call by Name: No reduction inside abstractions (Haskell)
Synopsis
- data Term
- tru :: Term
- fls :: Term
- c0 :: Term
- c2 :: Term
- apps :: [Term] -> Term
- land :: Term
- expr :: Term
- data ITerm
- deBruijnIndices :: [String] -> Term -> ITerm
- termShift :: Int -> ITerm -> ITerm
- termSubst :: Int -> ITerm -> ITerm -> ITerm
- termSubstTop :: ITerm -> ITerm -> ITerm
- isVal :: ITerm -> Bool
- eval :: ITerm -> ITerm
Documentation
Named lambda calculus representation. Grammar: term = x | λx.t | tt
Church boolean TRUE: λt.λf.t (returns first argument) >>> show tru "(|t.(|f.t))"
Church boolean FALSE: λt.λf.f (returns second argument) >>> show fls "(|t.(|f.f))"
Church numeral ZERO: λs.λz.z (successor applied 0 times) Based on Peano numbers: z=zero, s=successor function. >>> show c0 "(|s.(|z.z))"
Church numeral TWO: λs.λz.s(s z) (successor applied 2 times) >>> show c2 "(|s.(|z.(s (s z))))"
apps :: [Term] -> Term Source #
Builds left-associative applications from a list of terms. Allows us to write expression over expression, building complex applications. Takes multiple terms and combines them: apps [t1, t2, t3] = ((t1 t2) t3)
Logical AND for Church booleans: λb.λc.b c false >>> show land "(|b.(|c.((b c) (|t.(|f.f)))))"
Example expression: (land true true) >>> show expr "(((|b.(|c.((b c) (|t.(|f.f))))) (|t.(|f.t))) (|t.(|f.t)))"
Nameless lambda terms using De Bruijn indices (no variable names, just numbers).
deBruijnIndices :: [String] -> Term -> ITerm Source #
Converts named terms to De Bruijn indices. ctx: free variable names (context) - not bound within the term. Walk the term with empty stack initially. When numbering, we go from inside to inside, stacking variable names as we enter abstractions (n : stack). findInd checks stack first (bound vars), then context (free vars). For context variables: take context position + length of stack to renumber properly.
termShift :: Int -> ITerm -> ITerm Source #
Shifts free variables by d. Cutoff c tracks binding depth. Variables with index >= c are free and get shifted.
termSubst :: Int -> ITerm -> ITerm -> ITerm Source #
Substitutes term s for variable j. Core operation for beta reduction. When x == j+c, replace with s (shifted by c for binders).