evinism / evinism/lambda-explorer

Partial application

Offen
#126 1 Kommentar 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen
Vorherrschende Sprache
JavaScript
Sterne
69
Forks
10
PR-Merge-Kennzahlen
Keine gemergten PRs in 30 T.

Beschreibung

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

Beitragsleitfaden

Für dieses Repository ist kein Beitragsleitfaden indexiert

Bewertung

Dieses Issue wurde noch nicht bewertet.

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.