ljedrz / lambda_calculus Goto Github PK

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!

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?

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.

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().

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:

1. instruct the users to import church::* whenever they want to use non-numeric types (meh, that's just lazy)
2. import church functionalities into non-church modules (so much duplication)
3. create a module with common data encodings (getting warmer, but there is still a better way)
4. restructure the encoding modules so that the "types" are at the top level (aww yiss)

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:

• the encoding feature is easier to manage
• tests and benches can be done on a per-type basis (it's possible now, but the structure wouldn't be obvious); this would reduce the file count
• different numeral encodings can share common types

Disadvanages:

• quite a bit of work
• the conversions need to be re-thought
• slightly greater complexity

I'm open to suggestions; @billpmurphy?

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.
• It might also make sense to do something similar with the reduction steps for 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).
• It might be desirable to build the 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:

• A method is_supercombinator on Term that checks whether a lambda term is a supercombinator, i.e. just a depth-first search to check all the Vars.
• (more speculative) Since it's possible to Church-encode (or Scott-encode, etc) any algebraic data type, there could be a DSL for defining the "shape" of an algebraic datatype and then a function to convert this structure to lambda terms representing its Church-encoded (or Scott-encoded) constructors and accessors.

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.