GitHub - WhiteBlackGoose/LambdaCalculusFSharp: λ calculus library made purely in...
source link: https://github.com/WhiteBlackGoose/LambdaCalculusFSharp
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
λ calculus in F#
Library for lambda calculus made purely in and for F#
The λ-calculus is, at heart, a simple notation for functions and application. The main ideas are applying a function to an argument and forming functions by abstraction. Despite its sparse syntax, the expressiveness and flexibility of the λ-calculus make it a cornucopia of logic and mathematics. (c)
The library serves no production purpose and made exclusively out of academic interest. It has a web app made for demonstration.
Syntax of λ-calculus
Rules:
- Variables are single-character lower-case Latin letters.
- Lambda starts with
\
, then is followed by 1 or more variable, then a dot (.
), then expression. - Associativity is left-sided:
xyz
is(xy)z
. - A nested lambda can be shortcuted:
\x.\y.\z.xyz
is the same as\xyz.xyz
. - Symbol
λ
can be used instead of\
, but is not essential.
Examples:
x
- an expression of one free variable xxy
-y
applied tox
\x.x
- an identity\x.xx
- a lambda which returns its only parameter applied to itself(\x.x)y
-y
applied to identity (will returny
after beta reduction)(\x.xx)(\x.xx)
- simple example of beta-irreducible expression
Library API
Expression is defined as following:
type Expression = | Variable of char | Lambda of Head : Variable * Body : Expression | Applied of Lambda : Expression * Argument : Expression
in LambdaCalculus.Atoms
.
In the same module LambdaCalculus.Atoms
there are
betaReduce
orβReduce
:Expression -> Expression
performs beta-reduction, that is, simplification of an expression (starting from bottom, replaces parameters of lambdas in their bodies with the applied expressions)alphaEqual
orαEqual
:Expression -> Expression -> Expression
compares two expressions up to lambdas parameter namessubstitute
:char -> Expression -> Expression -> Expression
replaces the given variable with a given expression. In case of conflicts between it and a local variable in a lambda, it will alpha-convert the lambda's parameter to a new name.
In the module LambdaCalculus.Parsing
there is parse
which takes a string as an argument, and returns a Result
of
Expression
and string
.
Basic functions
Taken from Wikipedia.
Numbers
Number Lambda 0\fx.x
1
\fx.fx
2
\fx.f(fx)
3
\fx.f(f(fx))
4
\fx.f(f(f(fx)))
5
\fx.f(f(f(f(fx))))
6
\fx.f(f(f(f(f(fx)))))
7
\fx.f(f(f(f(f(f(fx))))))
8
\fx.f(f(f(f(f(f(f(fx)))))))
9
\fx.f(f(f(f(f(f(f(f(fx))))))))
Arithmetic operations
Operation Lambda Succ\nfx.f(nfx)
Plus
\mnfx.mf(nfx)
Mult
\mnfx.m(nf)x
Exp
\mn.nm
Pred
\nfx.n(\gh.h(gf))(\u.x)(\u.u)
Fun facts
The library is made in pure functional programming. Even the parser has no exceptions, early returns, for-loops. The logic is implemented with recursion, pattern matching, and computation expressions.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK