ljedrz / lambda_calculus Goto Github PK
View Code? Open in Web Editor NEWA simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust
License: Creative Commons Zero v1.0 Universal
A simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust
License: Creative Commons Zero v1.0 Universal
The following list functions cause issues in the doctests when used with Scott/Parigot/Stump-Fu numerals:
filter
foldl
foldr
index
length
list
map
take
take_while
(builds with Parigot/Stump-Fu)zip_with
This doesn't necessarily mean that the functions are not general enough - it might be the doctests' fault. The list integration test module needs to be extended with other encodings.
As Stump and Fu state in section 3 Previous Lambda Encodings:
We elide the definitions of basic non-recursive datatypes for pair types, sum types, booleans, the unit type, and a maybe type. Because these are not recursive, the different lambda-encodings all agree for them.
This means there is room for a refactoring of the encoding modules; right now 4 options come to mind:
church::*
whenever they want to use non-numeric types (meh, that's just lazy)The hierarchy could look as follows:
src
|- combinators.rs
|- lib.rs
|- parser.rs
|- reduction.rs
|- term.rs
|- data (or encoding?)
|- boolean.rs
|- list (a good moment to include additional list encodings)
|- one_pair.rs
|- two_pair.rs
|- rfold.rs
|- mod.rs
|- numerals
|- church.rs
|- mod.rs
|- parigot.rs
|- scott.rs
|- stumpfu.rs
|- option.rs
|- pair.rs
Advantages:
encoding
feature is easier to manageDisadvanages:
I'm open to suggestions; @billpmurphy?
As it is, lambda_calculus::term::PRETTY_LAMBDA
is a constant and you can only update it if you manually change the crate's source code. This means anyone wanting to use your crate can't actually choose whether to use the unicode λ
or a \
.
You may want to either make it a mutable static or provide some getters and setters so anyone using your crate can change it in their code without needing to make their own fork.
Just a little nitpicking because I saw you were wanting to do a 1.0 release on reddit. Other than that this looks like a really cool experiment!
According to Demonstrating Lambda Calculus Reduction by P. Sestoft, call-by-value (7.3) and hybrid applicative (7.5) β-reduction strategies should be able to work with the call-by-value fixed-point combinator, e.g. Y ≡ λh.(λx.λa.h (x x) a)(λx.λa.h (x x) a)
.
Some of such expressions, however, cause endless loops; this happens with div()
, quot()
, rem()
, factorial()
and other functions using the strict Z combinator z()
.
Some thoughts on API changes that might be nice to have in version 2.0.0; I'm happy to implement some or all of these.
compare
should return a data structure containing the reduction counts instead of writing to stdout. This data structure could have a Debug
and/or Display
implementation that returns a String that is the same as what compare
currently prints.beta
. This would probably require splitting beta
into two functions, beta
(which returns the reduced Term
) and beta_verbose
(which returns the reduced Term
and reduction steps).church
and scott
modules at the same time; the only functionality in those modules that needs to be hidden behind feature
gates are the From
implementations, as they conflict with each other. There are several ways to achieve this, one way would be to add functions like to_church_int
and to_scott_int
which can be compiled together, then just modify the From
implementations to call these.Some other non-breaking features that I think would be nice to have, not necessarily in 2.0.0:
is_supercombinator
on Term
that checks whether a lambda term is a supercombinator, i.e. just a depth-first search to check all the Var
s.I'm a newcomer to lambda calculus.
https://link.springer.com/content/pdf/10.1007/BF02458289.pdf, Figure 1a
The authors study the two expressions:
\a.(a)\b.\c.(c)\d.\e.(e)d
\a.(a)\b.\c.(c)b
Such that the application of one on the other replicates the expressions. I can't seem to do that with this program. Parsing the first expression:
Original string: \a.(a)\b.\c.(c)\d.\e.(e)d
Parsed expression (not reduced): \a.\b.\c.\d.\e.e e e d
Reduced expression is same as above: \a.\b.\c.\d.\e.e e e d
Parsing the second expression similarly gets me
Original string: \a.(a)\b.\c.(c)b
Parsed expression (not reduced): \a.\b.\c.c c b
Reduced expression is same as above: \a.\b.\c.c c b
I'm not able to replicate the results of the original paper.
What am I doing wrong?
With the latest PR I've noticed one potential improvement that is unlikely to ever be truly needed, but would make the library more airtight; unfortunately it would break the API, so it will need to wait for a 4.0
release. Therefore, I'm opening this issue to list any such potential future changes, and I'll be collecting them into a dedicated branch.
Breaking changes (a checkmark indicates that the 4.0
branch already contains the item):
usize
from Term::max_depth
const
-ify some of the functionsCc @AgentElement if there are any other breaking changes you'd like to see in the future or if you'd like to contribute any of the above
Binary numerals are almost ready, but their succ
and pred
functions produce unexpected results in tests, even though they are defined as specified in the paper by T. Mogensen.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.