¿Cuál es el equivalente lógico combinatorio de la teoría de tipos intuicionistas?

87

Recientemente completé un curso universitario que incluía Haskell y Agda (un lenguaje de programación funcional de tipo dependiente), y me preguntaba si era posible reemplazar el cálculo lambda en estos con lógica combinatoria. Con Haskell, esto parece posible usando los combinadores S y K, lo que lo hace sin puntos. Me preguntaba cuál era el equivalente para Agda. Es decir, ¿se puede hacer que un lenguaje de programación funcional de tipo dependiente 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 forma de eliminar la cuantificación universal de una firma de tipo sin cambiar su significado? Por ejemplo, en:

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

¿Se puede expresar lo mismo sin usar un forall?

haskell types functional-programming logic agda Grasevski
fuente
21
Empiece por averiguar los tipos más dependientes posibles para K (fácil) y S (bastante peludo). Sería interesante agregar constantes para Set y Pi, luego intentar reconstruir el sistema básico (inconsistente) Set: Set. Pensaría más, pero tengo que tomar un avión.
trabajador porcino

Respuestas:

52

Así que lo pensé un poco más y logré algunos avances. Aquí hay un primer intento de codificar la deliciosamente simple (pero inconsistente) de Martin-LöfSet : Set 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 cálculo lambda con anotaciones de tipos, tipos Pi y un conjunto de universos.

La teoría del tipo de objetivo

En aras de la integridad, presentaré las reglas. La validez de contexto simplemente dice que puede construir contextos desde vacíos al agregar variables nuevas que habitan en Sets.

                     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 hecho de lambda el único operador de enlace, por lo que el segundo argumento de Pi debería ser una función que calcule 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 puede dejar las abstracciones sin corchetes cuando son el último argumento de un operador de orden superior: puede ver que lo hice eso con Pi. Su tipo de Agda se (x : S) -> Tconvierte en Pi S \ x:S -> T.

( Digresión . Las anotaciones de tipo en lambda son necesarias si desea poder sintetizar el tipo de abstracciones. Si cambia a la verificación de tipo como su modus operandi, todavía necesita anotaciones para comprobar un tipo beta-redex (\ x -> t) s, ya que no tiene forma para adivinar los tipos de las partes del todo. Aconsejo a los diseñadores modernos que verifiquen los tipos y excluyan los beta-redexes de la sintaxis).

( Digresión . Este sistema es inconsistente ya que Set:Setpermite la codificación de una variedad de "paradojas del mentiroso". Cuando Martin-Löf propuso esta teoría, Girard le envió una codificación de la misma en su propio Sistema U inconsistente. La paradoja subsiguiente debida a Hurkens es la construcción tóxica más ordenada que conocemos.)

Sintaxis y normalización del combinador

De todos modos, tenemos dos símbolos adicionales, Pi y Set, por lo que quizás podríamos 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):

data SKUP = S | K | U | P deriving (Show, Eq)

data Unty a
  = C SKUP
  | Unty a :. Unty a
  | V a
  deriving (Functor, Eq)
infixl 4 :.

Tenga en cuenta que he incluido los medios para incluir variables libres representadas por tipo aen esta sintaxis. Además de ser un reflejo de mi parte (cada sintaxis digna de ese nombre es una mónada libre con returnvariables de incrustación y >>=sustitució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 exactamente para las formas normales y afinar 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 a la manera de Bellegarde y Hook (como popularizaron Bird y Paterson). El tipo Su atiene un elemento más que a, y lo usamos como el tipo de variables libres debajo de una carpeta, con Zecomo la nueva variable enlazada y Su xsiendo la representación desplazada de la antigua variable libre x.

Traducir términos a combinadores

Y una vez hecho esto, 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

Escribir los combinadores

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. Uy Pson solo constructores de conjuntos, por lo que, escribiendo tipos sin traducir y permitiendo la "notación Agda" para Pi, deberíamos tener

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

El Kcombinador se usa para elevar un valor de algún tipo Aa una función constante sobre algún otro tipo G.

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

El Scombinador se utiliza para levantar aplicaciones sobre un tipo, del que pueden depender todas las piezas.

  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 eso es lo que la hace adecuada para reflejar la construcción de la aplicación. ¡Ese es su trabajo!

Entonces tenemos 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 combinadores en la teoría de tipos ordinarios, no en la teoría de tipos combinatorios. 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 todo su esplendor ilegible: ¡una presentación combinatoria de Set:Set!

Todavía hay un pequeño problema. La sintaxis del sistema no le da ninguna manera de adivinar el G, Ay Bparámetros para Sy de manera similar para K, sólo de los términos. En consecuencia, podemos verificar las derivaciones de tipificación algorítmicamente, pero no podemos simplemente verificar los términos del combinador como podríamos hacer con el sistema original. Lo que podría funcionar es requerir que la entrada del comprobador de tipos lleve 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 detenerse, si ha tenido las ganas de comenzar. El resto son cosas "detrás de escena".

Generando los tipos de combinadores

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

Puedo escribir los tipos de combinadores, completamente abstraídos sobre sus parámetros, de la siguiente manera. Hago uso de mi práctica pilfunción, que combina Pi y lambda para evitar la repetición del tipo de dominio, y de manera bastante útil 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 subterráneos abiertos relevantes y los pasé a través de la traducción.

Un kit de herramientas de codificación de Bruijn

He aquí cómo construir pil. En primer lugar, defino una clase de Finconjuntos de ite, utilizados para variables. Cada uno de estos conjuntos tiene un embedding que preserva el constructor en el conjunto anterior, además de un nuevo topelemento, y puede diferenciarlos: la embdfunción 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, instantiate Finpara ZeySuc

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 iguales, con una operación de debilitamiento .

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

La wkfunción debe incrustar los elementos de xcomo los elementos más grandes de y, de modo que las cosas adicionales en ysean más pequeñas y, por lo tanto, en términos del índice de Bruijn, se limiten 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 resuelto eso, un poco de engaño de cráneos 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 sea visible. Es decir, el hecho de que me tome la molestia de distinguir los diferentes ámbitos por tipo le da al verificador de tipos de Haskell suficiente información para calcular el desplazamiento requerido para la traducción a la representación de Bruijn. ¿Por qué tener un perro y ladrar?

trabajador porcino
fuente
esto puede ser muy tonto, pero ¿cómo cambia esta imagen si agrega el Fcombinador? Factúa de manera diferente dependiendo de su primer argumento: Si Aes un átomo, My Nson términos y PQes un compuesto, entonces FAMN -> My F(PQ)MN -> NPQ. Esto no se puede representar en SK(I)cálculo, pero Kse puede representar como FF. ¿Es posible extender su MLTT sin puntos con esto?
kram1032
Estoy bastante seguro de que hay un problema con este procedimiento de abstracción de corchetes, específicamente la parte "los combinadores se vuelven constantes", que traduce λx.c en Kc para los combinadores c ∈ {S, K, U, P}. El problema es que estos combinadores son polimórficos y pueden usarse en un tipo que depende de x; este tipo no se puede conservar con esta traducción. Como ejemplo concreto, el término λ (A : Set) → λ (a : A) → ade tipo (A : Set) → (a : A) → Ase traduce a S(S(KS)(KK))(KK), que no se puede usar en un tipo donde el tipo del segundo argumento depende del primer argumento.
Anders Kaseorg
8

Supongo que la "Abstracción de soporte" también funciona para tipos dependientes en algunas circunstancias. En la sección 5 del siguiente documento, encontrará algunos tipos K y S:

Coincidencias escandalosas pero significativas
Evaluación y sintaxis dependiente de tipo seguro
Conor McBride, Universidad de Strathclyde, 2010

Convertir una expresión lambda en una expresión combinatoria corresponde aproximadamente a convertir una prueba de deducción natural en una prueba de estilo Hilbert.

Colapso de Mostowski
fuente