[BUG] Fix convert_classic_tokens

[hiratara]

"a b", the classical notation containing two free variables, should be converted to "12" in DeBruijn notation, but the current implementation converts it to "11". This PR fixes the problem.

Note that "(λa. a) (λa. a) a" can be converted to "(λ1)(λ1)2", but for simplicity of implementation, I convert it to "(λ1)(λ1)3". This is because I'm simply counting the number of appearances, not the maximum depth of λ-abstraction.

[hiratara]

The maximum depth of the stack is less than the number of appearances of the lambda abstract.

The number of free variables is less than the number of tokens minus the number of lambda abstractions.

[ljedrz]

Thanks for another contribution!

If I'm understanding this correctly (my lambda calculus skills are a bit rusty), ideally the term

(λm.λn.λs.λz. m s (n s z)) (λs.λz. z) (λs.λz. s z) s z

would translate to

(λλ(λλ1)2((λλ21)21))89

right? If that is the case, I'd just add an appropriate TODO comment to the 2 test cases where that expression is present, and one in convert_classic_tokens indicating that the current impl can still be improved. A new test case "(λa. a) (λa. a) a" == "(λ1)(λ1)2" that is currently marked as #[ignore = "TODO"] would also be a nice addition.

[hiratara]

There is no doubt that there are bugs in the current implementation, but the test cases are certainly not correct if you ask me.
I am interested in this issue and will do some more research and try to create a correct test case. Please wait a while 🙂

[hiratara]

I read the N.G. de Bruijn's original paper, rewrote this PR, and did push --force into my branch. In case you are wondering about the difference from the previous commit, it can be seen below.

https://github.com/hiratara/lambda_calculus/compare/57fc702166f122aa6663a2c82fe29087e4f23dbd..fix-free-vars

(λm.λn.λs.λz. m s (n s z)) (λs.λz. z) (λs.λz. s z) s z
would translate to
(λλ(λλ1)2((λλ21)21))89
right?

It depends on what we assume the free variable list to be. If we assume it is [..., z, s, x7, x6, x5, x4, x3, x2, x1], (λλ(λλ1)2((λλ21)21))89 is a correct namefree expression. If we assume it is [..., z, s], (λλ(λλ1)2((λλ21)21))12 is a correct namefree expression.

I added a test that failed in the previous commit. We need to adjust references to free variables according to the depth of the lambda abstraction.

lambda_calculus/tests/parser.rs

Lines 16 to 21 in 190c29f

	(
	// See: http://alexandria.tue.nl/repository/freearticles/597619.pdf
	"λ2(λ421(5(λ4127)λ8))67",
	// the free variable list is ..ywzfba
	"λx. a (λt. b x t (f (λu. a u t z) λs. w)) w y",
	),

[ljedrz]

Nice!

[ljedrz]

Apologies for the delayed merge; would you like me to release a bugfix version now?

[hiratara]

No, I am in no hurry. If you have other things to tweak, release them when you are done.