Skip to content

Commit a0d8132

Browse files
MorganCaronMorganCaron
committed
Functional: Lambda Calculus
1 parent c6dc531 commit a0d8132

3 files changed

Lines changed: 370 additions & 0 deletions

File tree

‎modules/CppUtils.mpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ export import CppUtils.Chrono;
55
export import CppUtils.Container;
66
export import CppUtils.Execution;
77
export import CppUtils.FileSystem;
8+
export import CppUtils.Functional;
89
export import CppUtils.Language;
910
export import CppUtils.ChronoLogger;
1011
export import CppUtils.Logger;

‎modules/Functional/Functional.mpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
export module CppUtils.Functional;
2+
3+
export import CppUtils.Functional.LambdaCalculus;

‎modules/Functional/LambdaCalculus.mpp‎

Lines changed: 366 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,366 @@
1+
export module CppUtils.Functional.LambdaCalculus;
2+
3+
import std;
4+
import CppUtils.Type.Utility;
5+
6+
export namespace CppUtils::Functional::LambdaCalculus
7+
{
8+
namespace v1
9+
{
10+
inline constexpr auto True = [](auto x) { return [x](auto) { return x; }; };
11+
inline constexpr auto False = [](auto) { return [](auto y) { return y; }; };
12+
13+
static_assert(True(true)(false) == true);
14+
static_assert(False(true)(false) == false);
15+
static_assert(std::same_as<std::remove_const_t<decltype(True(True)(False))>, std::remove_const_t<decltype(True)>>);
16+
static_assert(std::same_as<std::remove_const_t<decltype(False(True)(False))>, std::remove_const_t<decltype(False)>>);
17+
18+
inline constexpr auto If = [](auto condition) { return [condition](auto t) { return [condition, t](auto f) { return condition(t)(f); }; }; };
19+
20+
static_assert(If(True)(true)(false) == true);
21+
static_assert(If(False)(true)(false) == false);
22+
static_assert(std::same_as<std::remove_const_t<decltype(If(True)(True)(False))>, std::remove_const_t<decltype(True)>>);
23+
static_assert(std::same_as<std::remove_const_t<decltype(If(False)(True)(False))>, std::remove_const_t<decltype(False)>>);
24+
25+
inline constexpr auto And = [](auto lhs, auto rhs) { return If(lhs)(rhs)(False); };
26+
27+
static_assert(std::same_as<std::remove_const_t<decltype(And(False, False))>, std::remove_const_t<decltype(False)>>);
28+
static_assert(std::same_as<std::remove_const_t<decltype(And(False, True))>, std::remove_const_t<decltype(False)>>);
29+
static_assert(std::same_as<std::remove_const_t<decltype(And(True, False))>, std::remove_const_t<decltype(False)>>);
30+
static_assert(std::same_as<std::remove_const_t<decltype(And(True, True))>, std::remove_const_t<decltype(True)>>);
31+
32+
inline constexpr auto Or = [](auto lhs, auto rhs) { return If(lhs)(True)(rhs); };
33+
34+
static_assert(std::same_as<std::remove_const_t<decltype(Or(False, False))>, std::remove_const_t<decltype(False)>>);
35+
static_assert(std::same_as<std::remove_const_t<decltype(Or(False, True))>, std::remove_const_t<decltype(True)>>);
36+
static_assert(std::same_as<std::remove_const_t<decltype(Or(True, False))>, std::remove_const_t<decltype(True)>>);
37+
static_assert(std::same_as<std::remove_const_t<decltype(Or(True, True))>, std::remove_const_t<decltype(True)>>);
38+
39+
inline constexpr auto Not = [](auto value) { return If(value)(False)(True); };
40+
41+
static_assert(std::same_as<std::remove_const_t<decltype(Not(False))>, std::remove_const_t<decltype(True)>>);
42+
static_assert(std::same_as<std::remove_const_t<decltype(Not(True))>, std::remove_const_t<decltype(False)>>);
43+
44+
static_assert(And(Not(False), Or(True, False))(true)(false) == true);
45+
static_assert(std::same_as<std::remove_const_t<decltype(And(Not(False), Or(True, False))(True)(False))>, std::remove_const_t<decltype(True)>>);
46+
47+
inline constexpr auto Successor = [](auto n) { return [n](auto f) { return [n, f](auto x) { return f(n(f)(x)); }; }; };
48+
inline constexpr auto Zero = False;
49+
inline constexpr auto Count = [](auto c) { return c + 1; };
50+
51+
static_assert(not std::same_as<std::remove_const_t<decltype(Successor(Zero))>, std::remove_const_t<decltype(Zero)>>);
52+
static_assert(Zero(Count)(0uz) == 0uz);
53+
static_assert(Successor(Zero)(Count)(0uz) == 1uz);
54+
static_assert(Successor(Successor(Zero))(Count)(0uz) == 2uz);
55+
56+
inline constexpr auto Add = [](auto lhs, auto rhs) { return lhs(Successor)(rhs); };
57+
58+
static_assert(std::same_as<std::remove_const_t<decltype(Add(Zero, Zero))>, std::remove_const_t<decltype(Zero)>>);
59+
static_assert(Add(Zero, Zero)(Count)(0uz) == 0uz);
60+
61+
static_assert(std::same_as<std::remove_const_t<decltype(Add(Zero, Successor(Zero)))>, std::remove_const_t<decltype(Successor(Zero))>>);
62+
static_assert(Add(Zero, Successor(Zero))(Count)(0uz) == 1uz);
63+
64+
static_assert(std::same_as<std::remove_const_t<decltype(Add(Successor(Zero), Successor(Zero)))>, std::remove_const_t<decltype(Successor(Successor(Zero)))>>);
65+
static_assert(Add(Successor(Zero), Successor(Zero))(Count)(0uz) == 2uz);
66+
67+
inline constexpr auto Mult = [](auto lhs, auto rhs) { return [lhs, rhs](auto f) { return lhs(rhs(f)); }; };
68+
69+
static_assert(Mult(Successor(Successor(Zero)), Successor(Successor(Zero)))(Count)(0uz) == 4uz);
70+
}
71+
72+
inline namespace v2
73+
{
74+
template<std::size_t Index> // De Bruijn index
75+
struct Variable final
76+
{};
77+
78+
template<class Body>
79+
struct Lambda final
80+
{};
81+
82+
template<class Function, class Argument>
83+
struct Application final
84+
{};
85+
86+
template<class Expression, class Value, std::size_t Depth>
87+
struct Substitute final
88+
{
89+
using type = Expression;
90+
};
91+
92+
template<std::size_t Index, class Value, std::size_t Depth>
93+
struct Substitute<Variable<Index>, Value, Depth> final
94+
{
95+
using type = std::conditional_t<Index == Depth, Value, Variable<Index>>;
96+
};
97+
98+
template<class Body, class Value, std::size_t Depth>
99+
struct Substitute<Lambda<Body>, Value, Depth> final
100+
{
101+
using type = Lambda<typename Substitute<Body, Value, Depth + 1>::type>;
102+
};
103+
104+
template<class Function, class Argument, class Value, std::size_t Depth>
105+
struct Substitute<Application<Function, Argument>, Value, Depth> final
106+
{
107+
using type = Application<
108+
typename Substitute<Function, Value, Depth>::type,
109+
typename Substitute<Argument, Value, Depth>::type>;
110+
};
111+
112+
static_assert(std::is_same_v<
113+
typename Substitute<Variable<0>, Variable<42>, 0>::type,
114+
Variable<42>>);
115+
static_assert(std::is_same_v<
116+
typename Substitute<Lambda<Variable<1>>, Variable<42>, 0>::type,
117+
Lambda<Variable<42>>>);
118+
static_assert(std::is_same_v<
119+
typename Substitute<Lambda<Lambda<Variable<2>>>, Variable<42>, 0>::type,
120+
Lambda<Lambda<Variable<42>>>>);
121+
static_assert(std::is_same_v<
122+
typename Substitute<Application<Lambda<Variable<1>>, Variable<21>>, Variable<42>, 0>::type,
123+
Application<Lambda<Variable<42>>,
124+
Variable<21>>>);
125+
static_assert(std::is_same_v<
126+
typename Substitute<Application<Lambda<Variable<21>>, Variable<0>>, Variable<42>, 0>::type,
127+
Application<Lambda<Variable<21>>,
128+
Variable<42>>>);
129+
130+
template<class Expression>
131+
struct BetaReduction final
132+
{
133+
using type = Expression;
134+
};
135+
136+
template<class Body, class Argument>
137+
struct BetaReduction<Application<Lambda<Body>, Argument>> final
138+
{
139+
using type = typename Substitute<Body, Argument, 0>::type;
140+
};
141+
142+
template<class Expression, class Argument0, class Argument1>
143+
struct BetaReduction<Application<Application<Expression, Argument1>, Argument0>> final
144+
{
145+
using type = typename BetaReduction<Application<typename BetaReduction<Application<Expression, Argument1>>::type, Argument0>>::type;
146+
};
147+
148+
static_assert(std::is_same_v<
149+
typename BetaReduction<Variable<0>>::type,
150+
Variable<0>>);
151+
static_assert(std::is_same_v<
152+
typename BetaReduction<Lambda<Variable<0>>>::type,
153+
Lambda<Variable<0>>>);
154+
static_assert(std::is_same_v<
155+
typename BetaReduction<Application<Lambda<Variable<0>>, Variable<1>>>::type, // (λa.a)b
156+
Variable<1> // b
157+
>);
158+
static_assert(std::is_same_v<
159+
typename BetaReduction<Application<Lambda<Variable<1>>, Variable<2>>>::type, // (λa.b)c
160+
Variable<1> // b
161+
>);
162+
163+
template<class Expression>
164+
struct NormalForm final
165+
{
166+
private:
167+
using Reduced = BetaReduction<Expression>::type;
168+
169+
public:
170+
using type = Type::LazyEvaluationType<not std::is_same_v<Expression, Reduced>, NormalForm, Reduced, std::type_identity<Reduced>>::type;
171+
};
172+
173+
template<class Body>
174+
struct NormalForm<Lambda<Body>> final
175+
{
176+
using type = Lambda<typename NormalForm<Body>::type>;
177+
};
178+
179+
static_assert(std::is_same_v<
180+
typename NormalForm<Variable<0>>::type, // a
181+
Variable<0> // a
182+
>);
183+
static_assert(std::is_same_v<
184+
typename NormalForm<Lambda<Variable<0>>>::type, // λa.a
185+
Lambda<Variable<0>> // λa.a
186+
>);
187+
static_assert(std::is_same_v<
188+
typename NormalForm<Application<Lambda<Variable<0>>, Variable<1>>>::type, // (λa.a)b
189+
Variable<1> // b
190+
>);
191+
static_assert(std::is_same_v<
192+
typename NormalForm<Application<Lambda<Variable<1>>, Variable<2>>>::type, // (λa.b)c
193+
Variable<1> // b
194+
>);
195+
196+
static_assert(std::is_same_v<
197+
typename NormalForm<Application<Application<Lambda<Lambda<Variable<1>>>, Variable<2>>, Variable<3>>>::type, // (λb.λa.b)c d
198+
Variable<2> // c
199+
>);
200+
static_assert(std::is_same_v<
201+
typename NormalForm<Application<Application<Lambda<Lambda<Variable<0>>>, Variable<2>>, Variable<3>>>::type, // (λb.λa.a)c d
202+
Variable<3> // d
203+
>);
204+
static_assert(std::is_same_v<
205+
typename NormalForm<Application<Lambda<Variable<0>>, Lambda<Lambda<Variable<0>>>>>::type, // (λa.a)(λb.λa.a)
206+
Lambda<Lambda<Variable<0>>> // λb.λa.a
207+
>);
208+
static_assert(std::is_same_v<
209+
typename NormalForm<Application<Lambda<Variable<0>>, Lambda<Lambda<Variable<1>>>>>::type, // (λa.a)(λb.λa.b)
210+
Lambda<Lambda<Variable<1>>> // λb.λa.b
211+
>);
212+
213+
template<class Lhs, class Rhs>
214+
inline constexpr bool areEqual = std::is_same_v<typename NormalForm<Lhs>::type, typename NormalForm<Rhs>::type>;
215+
216+
static_assert(areEqual<Application<Lambda<Variable<0>>, Variable<1>>, Variable<1>>); // (λa.a)b == b
217+
static_assert(areEqual<Lambda<Application<Lambda<Variable<0>>, Variable<1>>>, Lambda<Variable<1>>>); // λb.(λa.a)b == λb.b
218+
219+
using False = Lambda<Lambda<Variable<0>>>; // F = λb.λa.a = λba.a
220+
using True = Lambda<Lambda<Variable<1>>>; // T = λb.λa.b = λba.b
221+
222+
static_assert(not areEqual<True, False>);
223+
static_assert(areEqual<True, True>);
224+
static_assert(areEqual<False, False>);
225+
static_assert(areEqual<True, Lambda<Lambda<Variable<1>>>>);
226+
static_assert(areEqual<False, Lambda<Lambda<Variable<0>>>>);
227+
228+
// If = λb.λt.λf.b t f = λbtf.b t f
229+
using If =
230+
Lambda<
231+
Lambda<
232+
Lambda<
233+
Application<
234+
Application<Variable<2>, Variable<1>>,
235+
Variable<0>>>>>;
236+
237+
// If T T F = T T F = T
238+
// détail:
239+
// If T T F = (λbtf.b t f)T T F = T T F = (λba.b)(λba.b)(λba.a) = (λa.(λba.b))(λba.a) = λba.b = T
240+
static_assert(areEqual<
241+
Application<
242+
Application<
243+
Application<If, True>,
244+
True>,
245+
False>,
246+
True>);
247+
248+
// If F T F = F T F = F
249+
// détail:
250+
// If F T F = (λbtf.b t f)F T F = F T F = (λba.a)(λba.b)(λba.a) = (λa.a)(λba.a) = λba.a = F
251+
static_assert(areEqual<
252+
Application<
253+
Application<
254+
Application<If, False>,
255+
True>,
256+
False>,
257+
False>);
258+
259+
// And = λab.If a b F
260+
using And =
261+
Lambda<
262+
Lambda<
263+
Application<
264+
Application<
265+
Application<If, Variable<1>>,
266+
Variable<0>>,
267+
False>>>;
268+
269+
static_assert(areEqual<Application<Application<And, False>, False>, False>); // And F F = (λab.If a b F) F F = If F F F = F
270+
static_assert(areEqual<Application<Application<And, False>, True>, False>); // And F T = (λab.If a b F) F T = If F T F = F
271+
static_assert(areEqual<Application<Application<And, True>, False>, False>); // And T F = (λab.If a b F) T F = If T F F = F
272+
static_assert(areEqual<Application<Application<And, True>, True>, True>); // And T T = (λab.If a b F) T T = If T T F = T
273+
274+
// Or = λab.If a T b
275+
using Or =
276+
Lambda<
277+
Lambda<
278+
Application<
279+
Application<
280+
Application<If, Variable<1>>,
281+
True>,
282+
Variable<0>>>>;
283+
284+
static_assert(areEqual<Application<Application<Or, False>, False>, False>); // Or F F = (λab.If a T b) F F = If F T F = F
285+
static_assert(areEqual<Application<Application<Or, False>, True>, True>); // Or F T = (λab.If a T b) F T = If F T T = T
286+
static_assert(areEqual<Application<Application<Or, True>, False>, True>); // Or T F = (λab.If a T b) T F = If T T F = T
287+
static_assert(areEqual<Application<Application<Or, True>, True>, True>); // Or T T = (λab.If a T b) T T = If T T T = T
288+
289+
// Not = λa.If a F T
290+
using Not =
291+
Lambda<
292+
Application<
293+
Application<
294+
Application<If, Variable<0>>,
295+
False>,
296+
True>>;
297+
298+
static_assert(areEqual<Application<Not, False>, True>); // Not F = (λa.If a F T) F = If F F T = T
299+
static_assert(areEqual<Application<Not, True>, False>); // Not T = (λa.If a F T) T = If T F T = F
300+
301+
template<class Expression>
302+
struct Evaluate;
303+
304+
template<>
305+
struct Evaluate<True>
306+
{
307+
static constexpr auto value = true;
308+
};
309+
310+
template<>
311+
struct Evaluate<False>
312+
{
313+
static constexpr auto value = false;
314+
};
315+
316+
using Zero = False;
317+
static_assert(areEqual<Zero, Lambda<Lambda<Variable<0>>>>);
318+
/*
319+
// Successor = λn.λf.λx.f((n f) x)
320+
using Successor =
321+
Lambda<
322+
Lambda<
323+
Lambda<
324+
Application<
325+
Variable<1>,
326+
Application<
327+
Application<Variable<2>, Variable<1>>,
328+
Variable<0>>>>>>;
329+
330+
static_assert(areEqual<Application<Successor, Zero>, Lambda<Lambda<Application<Variable<1>, Variable<0>>>>>);
331+
332+
// Add = λm.λn.λf.λx.m f (n f x)
333+
using Add =
334+
Lambda<
335+
Lambda<
336+
Lambda<
337+
Lambda<
338+
Application<
339+
Application<Variable<3>, Variable<1>>,
340+
Application<
341+
Application<Variable<2>, Variable<1>>,
342+
Variable<0>>>>>>>;
343+
static_assert(areEqual<
344+
Application<Application<Add, Zero>, Zero>,
345+
Zero>);
346+
static_assert(areEqual<
347+
Application<Application<Add, Zero>, Application<Successor, Zero>>,
348+
Application<Successor, Zero>>);
349+
static_assert(areEqual<
350+
Application<Application<Add, Application<Successor, Zero>>, Application<Successor, Zero>>,
351+
Application<Successor, Application<Successor, Zero>>>);
352+
353+
// Mult = λm.λn.λf. m (n f)
354+
using Mult =
355+
Lambda<
356+
Lambda<
357+
Lambda<
358+
Application<
359+
Variable<2>,
360+
Application<Variable<1>, Variable<0>>>>>>;
361+
static_assert(areEqual<
362+
Application<Application<Mult, Application<Successor, Application<Successor, Zero>>>, Application<Successor, Application<Successor, Zero>>>,
363+
Application<Successor, Application<Successor, Application<Successor, Application<Successor, Zero>>>>>); // Mult 2 2 = 4
364+
*/
365+
}
366+
}

0 commit comments

Comments
 (0)