haskell - temas - teoria del conocimiento intuicionismo

¿Cuál es el equivalente lógico combinatorio de la teoría de tipos intuicionista? (2)

Así que lo pensé un poco más e hice algunos progresos. Aquí hay una primera puñalada para codificar el sistema Set : Set deliciosamente simple (pero inconsistente) de Martin-Löf en un estilo combinatorio. No es una buena manera de terminar, pero es el lugar más fácil para comenzar. La sintaxis de esta teoría de tipos es simplemente lambda-cálculo con anotaciones de tipo, tipos Pi y un conjunto de universos.

La teoría del tipo de objetivo

Para mayor completud, presentaré las reglas. La validez del contexto solo dice que puedes construir contextos desde el vacío al adjuntar nuevas variables que habitan en Set s.

G |- valid G |- S : Set -------------- ----------------------------- x fresh for G . |- valid G, x:S |- valid

Y ahora podemos decir cómo sintetizar tipos para términos en cualquier contexto dado, y cómo cambiar el tipo de algo hasta el comportamiento computacional de los términos que contiene.

G |- valid G |- S : Set G |- T : Pi S / x:S -> Set ------------------ --------------------------------------------- G |- Set : Set G |- Pi S T : Set G |- S : Set G, x:S |- t : T x G |- f : Pi S T G |- s : S ------------------------------------ -------------------------------- G |- / x:S -> t : Pi S T G |- f s : T s G |- valid G |- s : S G |- T : Set -------------- x:S in G ----------------------------- S ={beta} T G |- x : S G |- s : T

En una pequeña variación del original, he convertido a lambda en el único operador de enlace, por lo que el segundo argumento de Pi debería ser una función que computa la forma en que el tipo de retorno depende de la entrada. Por convención (por ejemplo, en Agda, pero lamentablemente no en Haskell), el alcance de lambda se extiende hacia la derecha tanto como sea posible, por lo que a menudo puedes dejar abstracciones sin corchetes cuando son el último argumento de un operador de orden superior: puedes ver que lo hice eso con Pi. Su tipo de Agda (x : S) -> T convierte en Pi S / x:S -> T

( Digresión . Escriba las anotaciones en lambda si necesita poder sintetizar el tipo de abstracciones. Si cambia a la verificación de tipos como su modus operandi, aún necesita anotaciones para verificar una beta-redex como (/ x -> t) s , ya que no tiene forma de adivinar los tipos de las partes del total. Aconsejo a los diseñadores modernos que comprueben los tipos y excluyan los beta-redexes de la misma sintaxis).

( Digression . Este sistema es inconsistente ya que Set:Set permite la codificación de una variedad de "paradojas mentirosas." Cuando Martin-Löf propuso esta teoría, Girard le envió una codificación de ella en su propio inconsistente Sistema U. La paradoja subsecuente debida a Hurkens es la mejor construcción tóxica que conocemos).

Sintaxis y normalización del combinador

De todos modos, tenemos dos símbolos adicionales, Pi y Set, por lo que quizás podamos administrar una traducción combinatoria con S, K y dos símbolos adicionales: elegí U para el universo y P para el producto.

Ahora podemos definir la sintaxis combinatoria sin tipo (con variables libres):

Tenga en cuenta que he incluido los medios para incluir variables libres representadas por el tipo a en esta sintaxis. Además de ser un reflejo de mi parte (cada sintaxis digna de este nombre es una mónada gratuita con variables de inserción de return y >>= sustitución de ejecución), será útil representar etapas intermedias en el proceso de conversión de términos con enlace a su forma combinatoria.

Aquí está la normalización:

norm :: Unty a -> Unty a norm (f :. a) = norm f $. a norm c = c ($.) :: Unty a -> Unty a -> Unty a -- requires first arg in normal form C S :. f :. a $. g = f $. g $. (a :. g) -- S f a g = f g (a g) share environment C K :. a $. g = a -- K a g = a drop environment n $. g = n :. norm g -- guarantees output in normal form infixl 4 $.

(Un ejercicio para el lector es definir un tipo para exactamente las formas normales y agudizar los tipos de estas operaciones).

Representando la teoría de tipos

Ahora podemos definir una sintaxis para nuestra teoría de tipos.

data Tm a = Var a | Lam (Tm a) (Tm (Su a)) -- Lam is the only place where binding happens | Tm a :$ Tm a | Pi (Tm a) (Tm a) -- the second arg of Pi is a function computing a Set | Set deriving (Show, Functor) infixl 4 :$ data Ze magic :: Ze -> a magic x = x `seq` error "Tragic!" data Su a = Ze | Su a deriving (Show, Functor, Eq)

Utilizo una representación de índice de Bruijn en la forma de Bellegarde y Hook (popularizada por Bird y Paterson). El tipo Su a tiene un elemento más que a , y lo usamos como el tipo de variables libres bajo una carpeta, con Ze como la nueva variable ligada y Su x es la representación desplazada de la antigua variable libre x .

Traducir términos a Combinators

Y con eso hecho, adquirimos la traducción habitual, basada en la abstracción de corchetes .

tm :: Tm a -> Unty a tm (Var a) = V a tm (Lam _ b) = bra (tm b) tm (f :$ a) = tm f :. tm a tm (Pi a b) = C P :. tm a :. tm b tm Set = C U bra :: Unty (Su a) -> Unty a -- binds a variable, building a function bra (V Ze) = C S :. C K :. C K -- the variable itself yields the identity bra (V (Su x)) = C K :. V x -- free variables become constants bra (C c) = C K :. C c -- combinators become constant bra (f :. a) = C S :. bra f :. bra a -- S is exactly lifted application

Escribiendo los Combinators

La traducción muestra la forma en que usamos los combinadores, lo que nos da una pista sobre cuáles deberían ser sus tipos. U y P son constructores, por lo tanto, al escribir tipos no traducidos y permitir la "notación Agda" para Pi, deberíamos tener

U : Set P : (A : Set) -> (B : (a : A) -> Set) -> Set

El combinador K se usa para elevar un valor de algún tipo A a una función constante sobre algún otro tipo G

G : Set A : Set ------------------------------- K : (a : A) -> (g : G) -> A

El S combinator se usa para levantar aplicaciones sobre un tipo, del cual todas las partes pueden depender.

G : Set A : (g : G) -> Set B : (g : G) -> (a : A g) -> Set ---------------------------------------------------- S : (f : (g : G) -> (a : A g) -> B g a ) -> (a : (g : G) -> A g ) -> (g : G) -> B g (a g)

Si observa el tipo de S , verá que establece exactamente la regla de aplicación contextualizada de la teoría de tipos, por lo que es adecuada para reflejar la construcción de la aplicación. ¡Ese es su trabajo!

Entonces tenemos una aplicación solo para cosas cerradas

f : Pi A B a : A -------------- f a : B a

Pero hay un inconveniente. He escrito los tipos de los combinadores en la teoría de tipos ordinaria, no en la teoría de tipos combinatoria. Afortunadamente, tengo una máquina que hará la traducción.

Un sistema de tipo combinatorio

--------- U : U --------------------------------------------------------- P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU))) G : U A : U ----------------------------------------- K : P[A](S(S(KP)(K[G]))(S(KK)(K[A]))) G : U A : P[G](KU) B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU))) -------------------------------------------------------------------------------------- S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK)))) (S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A]))) (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G])))) (S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS))) (S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK)))) (S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK))) (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK))))))) M : A B : U ----------------- A ={norm} B M : B

Así que ahí lo tienes, en toda su gloria ilegible: una presentación combinatoria de Set:Set ¡ Set:Set !

Todavía hay un pequeño problema. La sintaxis del sistema no le permite adivinar los parámetros G , A y B para S y, de manera similar, para K , solo a partir de los términos. En consecuencia, podemos verificar derivaciones de tipado algorítmicamente, pero no podemos simplemente testear los términos del combinador como podríamos con el sistema original. Lo que podría funcionar es exigir que la entrada al registrador de tipos tenga anotaciones de tipo sobre los usos de S y K, registrando efectivamente la derivación. Pero esa es otra lata de gusanos ...

Este es un buen lugar para parar, si has sido lo suficientemente entusiasta como para comenzar. El resto está "detrás de escena".

Generando los tipos de los Combinators

Genere esos tipos combinatorios usando la traducción de abstracción de corchetes de los términos de teoría de tipos relevantes. Para mostrar cómo lo hice y hacer que esta publicación no sea del todo inútil, permítame ofrecerle mi equipo.

Puedo escribir los tipos de los combinadores, totalmente abstraídos sobre sus parámetros, de la siguiente manera. Hago uso de mi práctica función pil , que combina Pi y lambda para evitar repetir el tipo de dominio, y bastante útilmente me permite usar el espacio de funciones de Haskell para vincular variables. ¡Quizás casi puedas leer lo siguiente!

pTy :: Tm a pTy = fmap magic $ pil Set $ / _A -> pil (pil _A $ / _ -> Set) $ / _B -> Set kTy :: Tm a kTy = fmap magic $ pil Set $ / _G -> pil Set $ / _A -> pil _A $ / a -> pil _G $ / g -> _A sTy :: Tm a sTy = fmap magic $ pil Set $ / _G -> pil (pil _G $ / g -> Set) $ / _A -> pil (pil _G $ / g -> pil (_A :$ g) $ / _ -> Set) $ / _B -> pil (pil _G $ / g -> pil (_A :$ g) $ / a -> _B :$ g :$ a) $ / f -> pil (pil _G $ / g -> _A :$ g) $ / a -> pil _G $ / g -> _B :$ g :$ (a :$ g)

Con estos definidos, extraje los subtítulos abiertos relevantes y los ejecuté a través de la traducción.

A de Bruijn Encoding Toolkit

He aquí cómo construir pil . En primer lugar, defino una clase de conjuntos de iteraciones, utilizada para las variables. Cada uno de estos conjuntos tiene un editor de preservación de constructores en el conjunto anterior, más un nuevo elemento top , y usted puede distinguirlos: la función embd le dice si un valor está en la imagen de emb .

class Fin x where top :: Su x emb :: x -> Su x embd :: Su x -> Maybe x

Podemos, por supuesto, instanciar Fin para Ze y Suc

instance Fin Ze where top = Ze -- Ze is the only, so the highest emb = magic embd _ = Nothing -- there was nothing to embed instance Fin x => Fin (Su x) where top = Su top -- the highest is one higher emb Ze = Ze -- emb preserves Ze emb (Su x) = Su (emb x) -- and Su embd Ze = Just Ze -- Ze is definitely embedded embd (Su x) = fmap Su (embd x) -- otherwise, wait and see

Ahora puedo definir menos o igual, con una operación de debilitamiento .

class (Fin x, Fin y) => Le x y where wk :: x -> y

La función wk debe incorporar los elementos de x como los elementos más grandes de y , de modo que los elementos adicionales en y sean más pequeños, y por lo tanto en términos de índice de Bruijn, vinculados más localmente.

instance Fin y => Le Ze y where wk = magic -- nothing to embed instance Le x y => Le (Su x) (Su y) where wk x = case embd x of Nothing -> top -- top maps to top Just y -> emb (wk y) -- embedded gets weakened and embedded

Y una vez que hayas solucionado eso, un poco de skullduggery de rango-n hace el resto.

lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x lam s f = Lam s (f (Var (wk (Ze :: Su x)))) pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x pil s f = Pi s (lam s f)

La función de orden superior no solo le da un término que representa la variable, le da una cosa sobrecargada que se convierte en la representación correcta de la variable en cualquier ámbito donde la variable es visible. Es decir, el hecho de que me tome la molestia de distinguir los diferentes ámbitos por tipo le da al registrador de tipos Haskell suficiente información para calcular el desplazamiento requerido para la traducción a la representación de Bruijn. ¿Por qué mantener un perro y ladrar a ti mismo?

Hace poco terminé un curso universitario que presentaba Haskell y Agda (un lenguaje de programación funcional dependiente y mecanografiado), y me preguntaba si era posible reemplazar el cálculo lambda en estos con una lógica combinatoria. Con Haskell esto parece posible usando los combinadores S y K, por lo que es sin puntos. Me preguntaba cuál era el equivalente para Agda. Es decir, ¿se puede hacer que un lenguaje de programación funcional dependiente de tipo sea equivalente a Agda sin usar ninguna variable?

Además, ¿es posible reemplazar de alguna manera la cuantificación con combinadores? No sé si esto es una coincidencia, pero la cuantificación universal, por ejemplo, hace que una firma de tipo parezca una expresión lambda. ¿Hay alguna manera de eliminar la cuantificación universal de una firma tipo sin cambiar su significado? Ej. En:

forall a : Int -> a < 0 -> a + a < a

¿Se puede expresar lo mismo sin usar un forall?

Supongo que la "Resistencia de corchetes" también funciona para tipos dependientes en algunas circunstancias. En la sección 5 del siguiente artículo, encontrará algunos tipos K y S:

Coincidencias indignantes pero significativas
Dependencia de sintaxis segura y evaluación
Conor McBride, Universidad de Strathclyde, 2010

La conversión de una expresión lambda en una expresión combinatoria corresponde aproximadamente a la conversión de una prueba de deducción natural en una prueba de estilo de Hilbert.