¿Cómo ha añadido Haskell Turing-completeness al Sistema F?
He estado leyendo sobre varios sistemas de tipos y cálculos lambda, y veo que todos los cálculos lambda mecanografiados en el cubo lambda están fuertemente normalizando en lugar del equivalente de Turing. Esto incluye el Sistema F, el cálculo lambda simplemente tipado más polimorfismo.
Esto me lleva a las siguientes preguntas, para las cuales no he podido encontrar ninguna respuesta comprensible:
- ¿Cómo difiere el formalismo de (por ejemplo) Haskell del cálculo en el que se encuentra ¿aparentemente basada?
- ¿Qué características del lenguaje en Haskell no caen dentro del formalismo del Sistema F?
- ¿Cuál es el cambio mínimo necesario para permitir el cálculo completo de Turing?
Muchas gracias a quien me ayude a entender esto.
1 answers
En una palabra, recursión general.
Haskell permite la recursión arbitraria mientras que el Sistema F no tiene forma de recursión. La falta de tipos infinitos significa fix no es expresable como un término cerrado.
No hay noción primitiva de nombres y recursión. ¡De hecho, el Sistema F puro no tiene noción de ninguna cosa tal como definiciones!
Así que en Haskell esta sola definición es lo que añade integridad de turing
fix :: (a -> a) -> a
fix f = let x = f x in x
Realmente esta función es indicativa de una idea, al tener encuadernaciones totalmente recursivas, obtenemos turing completitud. Tenga en cuenta que esto se aplica a los tipos, no solo a los valores.
data Rec a = Rec {unrec :: Rec a -> a}
y :: (a -> a) -> a
y f = u (Rec u)
where u x = f $ unrec x x
Con tipos infinitos podemos escribir el combinador Y (modulo some unfolding) y a través de él recursión general!
En el Sistema F puro, a menudo tenemos alguna noción informal de definiciones, pero estas son simplemente abreviaturas que deben estar mentalmente integradas por completo. Esto no es posible en Haskell ya que esto crearía términos infinitos.
El núcleo de Términos de Haskell sin ninguna noción de let, where o = es fuertemente normalizante, ya que no tenemos infinitos tipos. Incluso este término central cálculo no es realmente Sistema F. Sistema F tiene "grandes lambdas" o abstracción de tipo. El término completo para id en el Sistema F es
id := /\ A -> \(x : A) -> x
Esto se debe a que la inferencia de tipos para el Sistema F es indecidible! Anotamos explícitamente donde y cuando esperamos polimorfismo. En Haskell tal propiedad sería molesto, por lo que limitamos la potencia de Haskell. En particular, nunca inferimos un tipo polimórfico para un argumento Haskell lambda sin anotación (pueden aplicarse términos y condiciones). Esta es la razón por la que en ML y Haskell
let x = exp in foo
no es lo mismo que
(\x -> foo) exp
Incluso cuando exp no es recursivo! Este es el quid de la inferencia de tipo HM y el algoritmo W, llamado "generalización let".
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2014-08-12 04:40:40