evinism / evinism/lambda-explorer

Partial application

Abierto
#126 1 comentario 0 reacciones 0 asignados Ver en GitHub
Lenguaje dominante
JavaScript
Estrellas
69
Forks
10
Métricas de merge de PR
Sin PR fusionados en 30 d

Descripción

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

Guía de contribución

No hay ninguna guía de contribución indexada para este repositorio

Evaluación

Este issue todavía no se ha evaluado.

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.