1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54

-- Simple untyped lambda calculus interpreter using de Bruijin indices
-- WRONG: https://jameshfisher.com/2018/03/15/a-lambda-calculus-interpreter-in-haskell/
-- See STLC.lean for a better implementation

inductive Term where
  | A : Term → Term → Term
  | L : Term → Term
  | V : Nat → Term

partial def reduce : Term → Term
  | .A fn arg =>
    match reduce fn with
    | .L body =>
      let rec incr d
      | .A fn arg => .A (incr (d + 1) fn) (incr (d + 1) arg)
      | .L body => .L <| incr (d + 1) body
      | .V x => .V <| if d ≤ x then x + 1 else x
      let rec sub n s
      | .A fn arg => .A (sub n s fn) (sub n s arg)
      | .L body => .L <| sub (n + 1) (incr 0 s) body
      | .V x => if x = n then s else .V (if n < x then x - 1 else x)
      reduce <| sub 0 (reduce arg) body
    | other => .A other arg
  | other => other

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 reduce <| .A (.A (.A S K) I) (.A (.A K I) S)
#eval reduce <| .A (.A (.A S K) I) K

-- Doesn't terminate
-- #eval reduce <| .A Y I