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

-- Simple untyped lambda calculus interpreter using de Bruijin indices
-- 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

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, .L body => .L <| sub (n + 1) 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

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