search

evinism / lambda-explorer

Tutorial / REPL for the lambda calculus
https://lambdaexplorer.com/
MIT License
61 stars 9 forks source link

Partial application #126

Open Easyoakland opened 9 months ago

Easyoakland commented 9 months ago

NAND TRUE yields a function which works correctly (λf₂.λa.λb.f₂ba). But when using (NAND TRUE) TRUE get an incorrect result (λa.λb.a) which is different from manually writing (λf₂.λa.λb.f₂ba) TRUE which yields λa.λb.b.

Am I conceptualizing this incorrectly or is this a bug?

> TRUE
λa.λb.a
<function, church boolean true>
> NAND
λf₁.λf₂.λa.λb.f₁(f₂ba)a
<function>
> NAND TRUE
λf₂.λa.λb.f₂ba
<function>
> NAND TRUE TRUE
λa.λb.a
<function, church boolean true>
> (λf₂.λa.λb.f₂ba) TRUE
λa.λb.b
<function, church numeral 0, church boolean false>
> (NAND TRUE) TRUE
λa.λb.a
<function, church boolean true>
> (λf₂.λa.λb.f₂ba) TRUE
λa.λb.b
<function, church numeral 0, church boolean false>(-)
Free Variables:
Rendered from AST: (λf₂.λa.λb.f₂ba)(λa.λb.a)
Beta-reduced: λa.λb.(λa.λb.a)ba
Eta-reduced: [eta irreducible]
Normal Form: λa.λb.b
Normal As Church Numeral: 0
Normal As Church Boolean: false
steps to normal form:

    (λf₂.λa.λb.f₂ba)(λa.λb.a)
    λa.λb.(λa.λb.a)ba
    λa.λb.(λε₁.b)a
    λa.λb.b

> (NAND TRUE) TRUE
λa.λb.a
<function, church boolean true>
Free Variables:
Rendered from AST: (λf₁.λf₂.λa.λb.f₁(f₂ba)a)(λa.λb.a)(λa.λb.a)
Beta-reduced: [beta irreducible]
Eta-reduced: [eta irreducible]
Normal Form: λa.λb.a
Normal As Church Numeral: [not a church numeral]
Normal As Church Boolean: true
steps to normal form:

    (λf₁.λf₂.λa.λb.f₁(f₂ba)a)(λa.λb.a)(λa.λb.a)
    (λf₂.λa.λb.(λa.λb.a)(f₂ba)a)(λa.λb.a)
    λa.λb.(λa.λb.a)((λa.λb.a)ba)a
    λa.λb.(λε₁.(λa.λb.a)ba)a
    λa.λb.(λε₁.λb.a)ba
    λa.λb.(λε₁.a)a
    λa.λb.a
evinism commented 7 months ago

Likely related: https://github.com/evinism/lambda-explorer/issues/125