blob: 2db8051d2e02f334af86b746bbeb4ebe4a02ef2f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
#!/usr/bin/env elixir
###########
# LOGIC #
###########
_true = fn x -> fn y -> x end end
_false = fn x -> fn y -> y end end
_not = fn b -> b.(_false).(_true) end
_and = fn b1 -> fn b2 -> b1.(b2).(_false) end end
_or = fn b1 -> fn b2 -> b1.(_true).(b2) end end
#####################
# CHURCH NUMERALS #
#####################
_zero = fn f -> fn x -> x end end
_succ = fn n -> fn f -> fn x -> f.(n.(f).(x)) end end end
_pred = fn n ->
fn f ->
fn x ->
n.(fn g -> fn h -> h.(g.(f)) end end).(fn u -> x end).(fn a -> a end)
end
end
end
_one = _succ.(_zero)
########################################
# HELPERS - not pure lambda calculus #
########################################
read_bool = fn b -> IO.puts(b.("t").("f")) end
read_church = fn n -> IO.puts(n.(fn x -> x + 1 end).(0)) end
##############
# EXAMPLES #
##############
IO.puts("LOGIC")
IO.puts("--------------")
IO.puts("TRUE/FALSE")
# t
read_bool.(_true)
# f
read_bool.(_false)
IO.puts("NOT")
# f
read_bool.(_not.(_true))
# t
read_bool.(_not.(_false))
IO.puts("AND")
# t
read_bool.(_and.(_true).(_true))
# f
read_bool.(_and.(_true).(_false))
# f
read_bool.(_and.(_false).(_true))
# f
read_bool.(_and.(_false).(_false))
IO.puts("OR")
# t
read_bool.(_or.(_true).(_true))
# t
read_bool.(_or.(_true).(_false))
# t
read_bool.(_or.(_false).(_true))
# f
read_bool.(_or.(_false).(_false))
IO.puts("\nCHURCH NUMERALS")
IO.puts("--------------")
IO.puts("ZERO/SUCC")
# 0
read_church.(_zero)
# 1
read_church.(_succ.(_zero))
# 2
read_church.(_succ.(_succ.(_zero)))
# 3
read_church.(_succ.(_succ.(_succ.(_zero))))
IO.puts("PRED")
# 0
read_church.(_pred.(_one))
# 1
read_church.(_pred.(_succ.(_one)))
# 2
read_church.(_pred.(_succ.(_succ.(_one))))
|
