Skip to content

Some expressions don't reduce properly #1

@ftxqxd

Description

@ftxqxd

When trying to add a predecessor function, I encountered what appears to be a bug, which can be seen by uncommenting line 99 in parse.rs. Running 3 (func) (\l.l 0 0) gives the result (λz.((z (λy.(λx.(y (y (y x)))))) (λy.(λx.(y (y x)))))), which, when called with F (in a separate expression), gives the expected result of (λy.(λx.(y (y x)))) (2). However, running (3 (func) (\l.l 0 0)) F (all in one expression) results in (λs.(λz.z)) (0). These two results should be the same.

The problem seems to be in beta_reduce (removing eta_convert has no effect on the bug).

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions