Fix the incorrect untyped lambcalc thing

Changes

1 changed files (+38/-6)

• LambCalc.lean
  • @@ -1,21 +1,53 @@
    -- Simple untyped lambda calculus interpreter using de Bruijin indices - -- https://jameshfisher.com/2018/03/15/a-lambda-calculus-interpreter-in-haskell/ + -- WRONG: https://jameshfisher.com/2018/03/15/a-lambda-calculus-interpreter-in-haskell/ inductive Term where | A : Term → Term → Term | L : Term → Term | V : Nat → Term - def red : Term → Term + unsafe def red : Term → Term | .A fn arg => match red fn with | .L body => + let rec incr n d + | .A fn arg' => .A (incr n (d + 1) fn) (incr n (d + 1) arg') + | .L body => .L <| incr n (d + 1) body + | .V n' => .V <| if n' > d then n + n' else n' let rec sub - | n, .A fn arg => .A (sub n fn) (sub n arg) + | n, .A fn arg' => .A (sub n fn) (sub n arg') | n, .L body => .L <| sub (n + 1) body - | n, .V n' => if n = n' then arg else .V n' - sub 0 body + | n, .V n' => if n = n' then incr n 0 arg else .V n' + red <| sub 0 body | other => .A other arg | other => other - #eval red <| .A (.L (.V 69)) (.V 1) + def I := Term.L (.V 0) + + def K := Term.L <| Term.L (.V 1) + + def S := Term.L + (.L + (.L + (.A + (.A (.V 2) (.V 0)) + (.A (.V 1) (.V 0)) + ) + ) + ) + + def Y := Term.L + (.A + (.L + (.A (.V 1) (.A (.V 0) (.V 0))) + ) + (.L + (.A (.V 1) (.A (.V 0) (.V 0))) + ) + ) + + #eval red <| .A (.A (.A S K) I) (.A (.A K I) S) + #eval red <| .A (.A (.A S K) I) K + + -- Doesn't terminate + -- #eval red <| .A Y I