-
Notifications
You must be signed in to change notification settings - Fork 0
/
lambda_calculus.erl
157 lines (124 loc) · 3.37 KB
/
lambda_calculus.erl
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
%% Lambda calculus evaluator on Erlang
-module(lambda_calculus).
% -export([print/1, identity/0, y_combinator/0, test_lambda/0, apply/2]).
-export([print/1, identity/0, y_combinator/0, test_lambda/0]).
-export_type([]).
%%
%% TODO
%%
%% Implement Beta-Eta-Reduction
%% Implement Eval
%% Implement Apply
%% Implement Reduce
%% Implement Parser
%% Implement closures and defun
%%% Types
%% a lambda is the form
%% (\a.s-expression)
%%
%% the s-expression can be
%%
%% (\a.a) <- lambda
%%
%% (\a.a a)(\a.a a) <- abstraction
%% (\a.b)c <- also abstraction
%%
%% a <- a atom | with is also a symbol
%% asdfasdf <- also a atom
%%
%% where they need to have a environment on the lambda
%%
-type symbol() :: {'sym', atom()}.
-type s_expr() :: {'lambda', atom(), [s_expr()]}
| symbol()
| {'abstrac', s_expr(), s_expr()}.
-type env() :: [{symbol(), s_expr()}].
-type beta() :: {'beta', {symbol(), symbol()}}.
-type eta() :: {'eta', [beta()], s_expr()}.
%%
%% @doc print/1
%%
%% take a expression and convert to string
-spec print(s_expr()) -> string().
print({beta, {sym, A}, {sym,B}}) ->
"[" ++ atom_to_list(B) ++ "/" ++ atom_to_list(A) ++ "]";
print({lambda, {sym, Atm}, [Exhead|Extail]}) ->
"(\\" ++ atom_to_list(Atm) ++ "." ++ print(Exhead) ++ print(Extail) ++ ")";
print([Exhead|Extail]) ->
print(Exhead) ++ print(Extail);
print({abstrac, Ex1, Ex2}) ->
"(" ++ print(Ex1) ++ " " ++ print(Ex2) ++ ")";
print({eta, [HeadEnv|TailEnv], Exp}) ->
"(be" ++ print(HeadEnv) ++ print(TailEnv) ++ print(Exp) ++ ")";
print([]) ->
"";
print({sym, N}) ->
atom_to_list(N).
%% print(E) -> %% this needs to be commented for soundness
%% atom_to_list(E).
%%
%% @doc identity/0
%%
%% Identity s-expression
-spec identity() -> s_expr().
identity() ->
{lambda, {sym, a}, [{sym, a}]}.
%%
%% @doc y_combinator/0
%%
%% Y Combinator for my interpreter.
-spec y_combinator() -> s_expr().
y_combinator () ->
{abstrac, {lambda, {sym, a}, [{abstrac, {sym, a}, {sym, a}}]}, {lambda, {sym, a}, [{abstrac, {sym, a}, {sym, a}}]}}.
%%
%% @doc test_lambda/0
%%
%% Test Lambda Print Function.
-spec test_lambda() -> s_expr().
test_lambda() ->
{lambda, {sym, a}, [{sym, a}, {sym, a}, {lambda, {sym,x}, [{sym, y}]}]}.
%%
%% @doc reduce/2
%%
%% Apply beta reduction on one expression
-spec reduce(beta(), s_expr(), env()) -> s_expr().
reduce({beta, {sym,A}, {sym,B}}, {lambda, {sym,C}, [Exp]}, Env) ->
A.
%%
%% @doc apply
%%
%% Apply beta-eta reduction on a s-expression.
%% -spec apply(eta(), env()) -> s_expr().
%% apply() ->
%% nil.
%%
%% @doc eval/2
%%
%% Evaluator with no environment.
%% -spec eval(s_expr(),env()) -> beta().
%% eval({sym, N}, Env) ->
%% {beta, Env, {sym, N}};
%% eval({lambda, Atm, Ex}, Env) ->
%% {beta, Env, {lambda, Atm, Ex}};
%% eval({abstrac, {lambda, N, Exp1}, Exp2}, Env) ->
%% {beta, NExp, NEnv} = eval(Exp2, Env),
%% NEnv1 = NEnv ++ Env,
%% Exp2.
%% @doc lookup/2
%% Key in a list of key-value pairs.
%% Fails if the key not present.
-spec lookup(atom(),env()) -> integer().
lookup(A, {A,V}) ->
V;
lookup(A, [{A,V}|_]) ->
V;
lookup(A, [_|Rest]) ->
lookup(A,Rest).
%% @doc replace/3
%% replace caracters on erlang.
%% replace([], _, _) -> [];
%% replace([H|T], P, R) ->
%% [ if H =:= P -> R;
%% true -> H
%% end | replace(T, P, R)].
%%