evinism / evinism/lambda-explorer
Partial application
- Lingua principale
- JavaScript
- Stelle
- 69
- Fork
- 10
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Descrizione
`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
```
Guida per i contributori
Nessuna guida per i contributori indicizzata per questo repository
Valutazione
Questa issue non è ancora stata valutata.