¿Hay un cálculo de SKI mecanografiado?

La mayoría de nosotros conocemos la correspondencia entre la lógica combinatoria y el cálculo lambda . Pero nunca he visto (tal vez no he mirado lo suficientemente profundo) el equivalente de "combinadores mecanografiados", correspondiente al cálculo lambda simplemente mecanografiado. ¿Existe tal cosa? ¿Dónde se puede encontrar información al respecto?

reference-request logic lambda-calculus type-theory combinatory-logic Hugo Sereno Ferreira
fuente

Quizás te interese The Reader Monad y Abstraction Elimination en The Monad.Reader, número 17 . La mónada Reader (o más precisamente su functor aplicativo) está estrechamente relacionada con el SKI escrito.

Petr Pudlák

Respuestas:

Se ha demostrado la integridad expresiva de los combinadores mecanografiados en comparación con el cálculo lambda simplemente mecanografiado . Para cada combinador sin tipo, se necesita una familia completa de combinadores con tipo. Por ejemplo, uno tiene

$\mathbf{I}_{\alpha\to\alpha}$
$\mathbf{K}_{\alpha\to(\beta\to\alpha)}$
$\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\to\gamma))}$

para todas las combinaciones de tipos simples y . $\alpha,\beta$ $\gamma$

Alternativamente, solo piense en los tipos como esquemas de tipos (o tipos polimórficos) e ingréselos en Haskell y voila: combinadores .

Dave Clarke
fuente

¡Nunca pensé que el combinador

actuara sobre una mónada! ¿Es eso así?

S

$\mathbf{S}$

Hugo Sereno Ferreira

En realidad, he señalado que

corresponde al operador de aplicativos Functors, y el

S

$\mathbf{S}$ <*>pure

K

$\mathbf{K}$

Hugo Sereno Ferreira

es bastante fundamental, por lo que podría corresponder a muchas cosas.

tiene el mismo tipo como la función mónada

para funtor

S

$\mathbf{S}$

S

$\mathbf{S}$

a p

$ap$

Λ X . α \to X

$\Lambda X.\alpha\to X$

Dave Clarke