Czy istnieje pełny rachunek lambda na maszynie Turinga?

Tak, oczywiście. Wiele typowanych obliczeń lambda akceptuje z założenia tylko silnie normalizujące terminy, więc nie mogą one wyrażać dowolnych obliczeń. Ale system typów może być dowolny; uczyń go wystarczająco szerokim, abyś mógł wyrazić wszystkie obliczenia deterministyczne.

Trywialny system typów, który obejmuje fragment rachunku różniczkowego lambda zawierający Turinga, to taki, który akceptuje każdy termin równie dobrze wpisany (z najwyższym typem ).

\frac{}{Γ ⊢ M : ⊤}

$\dfrac{}{\Gamma \vdash M : \top}$

Mówiąc prościej, funkcjonalne języki programowania o statycznym typie mają u podstaw typowy rachunek lambda, który umożliwia także kombinację punktów stałych . Na przykład zacznij od prostego rachunku różniczkowego lambda (lub systemu typu ML, systemu F lub dowolnego innego systemu typów) i dodaj regułę, która tworzy kombinator punktów stałych, taki jak dobrze napisane. $\mathbf{Y} = \lambda f. (\lambda x. f (x\,x)) (\lambda x. f (x\,x))$ Reguły przedstawione powyżej są raczej niezdarne, ponieważ tworzą terminy takie jak

\frac{Γ ⊢ f : T \to T}{Γ ⊢ Y f : T} \frac{Γ ⊢ f : T \to T}{Γ ⊢ (λ x . f (x x)) (λ x . f (x x)) : T}

$\dfrac{\Gamma \vdash f : T \rightarrow T} {\Gamma \vdash \mathbf{Y}\,f : T} \qquad \dfrac{\Gamma \vdash f : T \rightarrow T} {\Gamma \vdash (\lambda x. f (x\,x)) (\lambda x. f (x\,x)) : T}$

dobrze napisane, chociaż ich składniki nie są dobrze napisane - nie są w pełni kompozycyjne. Prostą poprawką jest dodanie kombinacji punktów stałych jako stałej językowej i zapewnienie dla niej reguły delta; wtedy łatwo jest mieć system typów i semantykę redukcji zzachowaniem typu. Uciekasz od czystego rachunku lambda do królestwa rachunku lambda ze stałymi.

Y f

$\mathbf{Y}\,f$

\begin{matrix} \frac{}{Γ ⊢ fix : (T \to T) \to T} \\ fix f \to f (fix f) \end{matrix}

$\begin{gather*} \dfrac{}{\Gamma \vdash \textbf{fix} : (T \rightarrow T) \rightarrow T} \\ \textbf{fix}\,f \to f (\textbf{fix}\,f) \\ \end{gather*}$

Interesującym systemem typów jest rachunek różniczkowy lambda z typem przecięcia.

\frac{Γ ⊢ M : T_{1} Γ ⊢ M : T_{2}}{Γ ⊢ M : T_{1} \land T_{2}} (\land I) \frac{}{Γ ⊢ M : ⊤} (⊤ I)

$\dfrac{\Gamma \vdash M : T_1 \quad \Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \wedge T_2} (\wedge I) \qquad\qquad \dfrac{} {\Gamma \vdash M : \top} (\top I)$

Typy skrzyżowań mają interesujące właściwości w odniesieniu do normalizacji:

Termin lambda można wpisać bez użycia $\top I$
Termin lambda przyjmuje typ niezawierający $\top$

Zobacz Charakterystyka terminów lambda, które mają typy związków, aby dowiedzieć się, dlaczego typy skrzyżowań mają tak niezwykły zakres.

Masz więc system typów definiujący język Turinga (ponieważ każdy termin jest dobrze napisany) oraz prostą charakterystykę obliczeń kończących. Oczywiście, ponieważ ten typ systemu charakteryzuje normalizację, nie można go rozstrzygać.

_{$(\top I)$ $(\wedge I)$ $I$ $\wedge$ $\top$ $\rightarrow$ $\rightarrow$}

— Gilles „SO- przestań być zły”
źródło