Czy istnieje zapisany rachunek SKI?

Większość z nas zna zgodność między logiką kombinacyjną a rachunkiem lambda . Ale nigdy nie widziałem (może nie spojrzałem wystarczająco głęboko) odpowiednika „typowanych kombinatorów”, odpowiadającego po prostu typowanemu rachunku lambda. Czy coś takiego istnieje? Gdzie można znaleźć informacje na ten temat?

reference-request logic lambda-calculus type-theory combinatory-logic Hugo Sereno Ferreira
źródło

Być może zainteresują Cię The Reader Monad i Abstraction Elimination w The Monad.Reader, wydanie 17 . Monada Czytelnika (a ściślej jego funktor aplikacyjny) jest ściśle związana z typem SKI.

Petr Pudlák,

Odpowiedzi:

Wyrazisty kompletność wpisanych kombinatorów porównaniu do rachunku lambda po prostu wpisane zostało wykazane . Do każdego nietypowego kombinatora potrzebna jest cała rodzina kombinowanych typów. Na przykład jeden ma

$\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))}$

dla wszystkich kombinacji prostych typów i . $\alpha,\beta$ $\gamma$

Alternatywnie, pomyśl o typach jako o schematach typów (lub typach polimorficznych) i wprowadź je w Haskell i voila: kombinatory .

Dave Clarke
źródło

S

$\mathbf{S}$

S

$\mathbf{S}$ <*>pure

K

$\mathbf{K}$

S

$\mathbf{S}$

S

$\mathbf{S}$

a p

$ap$

Λ X . α \to X

$\Lambda X.\alpha\to X$