evinism / evinism/lambda-explorer

Partial application

Open
#126 1 comment 0 reactions 0 assignees View on GitHub
Dominant language
JavaScript
Stars
69
Forks
10
PR merge metrics
No merged PRs in 30d

Description

`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

> NAND
λf₁.λf₂.λa.λb.f₁(f₂ba)a

> NAND TRUE
λf₂.λa.λb.f₂ba

> NAND TRUE TRUE
λa.λb.a

> (λf₂.λa.λb.f₂ba) TRUE
λa.λb.b

> (NAND TRUE) TRUE
λa.λb.a

```

```
> (λf₂.λa.λb.f₂ba) TRUE
λa.λb.b
(-)
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

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
```

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.