Quel est l'équivalent en logique combinatoire de la théorie des types intuitionnistes?

Question 1

J'ai récemment terminé un cours universitaire qui présentait Haskell et Agda (un langage de programmation fonctionnel typé dépendant), et je me demandais s'il était possible de remplacer le calcul lambda dans ces derniers par la logique combinatoire. Avec Haskell, cela semble possible en utilisant les combinateurs S et K, ce qui le rend sans point. Je me demandais quel était l'équivalent pour Agda. Par exemple, peut-on créer un langage de programmation fonctionnel typé de manière dépendante équivalent à Agda sans utiliser de variables?

En outre, est-il possible de remplacer d'une manière ou d'une autre la quantification par des combinateurs? Je ne sais pas si c'est une coïncidence mais la quantification universelle par exemple fait ressembler une signature de type à une expression lambda. Existe-t-il un moyen de supprimer la quantification universelle d'une signature de type sans changer sa signification? Par exemple dans:

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

Peut-on exprimer la même chose sans utiliser un forall?

Question 2

J'y ai donc réfléchi un peu plus et j'ai progressé. Voici une première tentative d'encodage du système délicieusement simple (mais incohérent) de Martin-Löf Set : Setdans un style combinatoire. Ce n'est pas une bonne façon de terminer, mais c'est l'endroit le plus simple pour commencer. La syntaxe de cette théorie de type est juste un lambda-calcul avec des annotations de type, des types Pi et un ensemble d'univers.

La théorie du type de cible

Par souci d'exhaustivité, je vais présenter les règles. La validité de contexte indique simplement que vous pouvez créer des contextes à partir de vides en joignant de nouvelles variables habitant Sets.

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

Et maintenant, nous pouvons dire comment synthétiser des types pour des termes dans un contexte donné, et comment changer le type de quelque chose jusqu'au comportement de calcul des termes qu'il contient.

  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

Dans une petite variante de l'original, j'ai fait de lambda le seul opérateur de liaison, donc le deuxième argument de Pi devrait être une fonction calculant la façon dont le type de retour dépend de l'entrée. Par convention (par exemple dans Agda, mais malheureusement pas dans Haskell), la portée de lambda s'étend aussi loin que possible vers la droite, vous pouvez donc souvent laisser les abstractions sans crochets quand elles sont le dernier argument d'un opérateur d'ordre supérieur: vous pouvez voir que je l'ai fait cela avec Pi. Votre type Agda (x : S) -> Tdevient Pi S \ x:S -> T.

( Digression . Les annotations de type sur lambda sont nécessaires si vous voulez être capable de synthétiser le type d'abstractions. Si vous passez à la vérification de type comme modus operandi, vous avez toujours besoin d'annotations pour vérifier un beta-redex comme (\ x -> t) s, car vous n'avez aucun moyen pour deviner les types des parties de celui de l'ensemble. Je conseille aux concepteurs modernes de vérifier les types et d'exclure les beta-redex de la syntaxe même.)

( Digression . Ce système est incohérent car il Set:Setpermet le codage d'une variété de "paradoxes de menteur". Lorsque Martin-Löf a proposé cette théorie, Girard lui a envoyé un codage de celle-ci dans son propre système U incohérent. la construction toxique la plus soignée que nous connaissons.)

Syntaxe et normalisation du combinateur

Quoi qu'il en soit, nous avons deux symboles supplémentaires, Pi et Set, donc nous pourrions peut-être gérer une traduction combinatoire avec S, K et deux symboles supplémentaires: j'ai choisi U pour l'univers et P pour le produit.

Nous pouvons maintenant définir la syntaxe combinatoire non typée (avec des 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 :.

Notez que j'ai inclus les moyens d'inclure des variables libres représentées par type adans cette syntaxe. En plus d'être un réflexe de ma part (toute syntaxe digne de ce nom est une monade libre avec des returnvariables d'intégration et >>=une substitution performante), il sera pratique de représenter des étapes intermédiaires dans le processus de conversion des termes avec liaison à leur forme combinatoire.

Voici la normalisation:

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 exercice pour le lecteur consiste à définir un type pour exactement les formes normales et à affiner les types de ces opérations.)

Représenter la théorie des types

Nous pouvons maintenant définir une syntaxe pour notre théorie des types.

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)

J'utilise une représentation d'index de Bruijn à la manière Bellegarde et Hook (telle que popularisée par Bird et Paterson). Le type Su aa un élément de plus que a, et nous l'utilisons comme type de variables libres sous un classeur, avec Zecomme variable nouvellement liée et Su xétant la représentation décalée de l'ancienne variable libre x.

Traduire les termes en combinateurs

Et avec cela fait, nous acquérons la traduction habituelle, basée sur l' abstraction des crochets .

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

Saisir les combinateurs

La traduction montre la façon dont nous utilisons les combinateurs, ce qui nous donne un indice sur ce que devraient être leurs types. Uet ne Psont que des constructeurs définis, donc, en écrivant des types non traduits et en permettant la "notation Agda" pour Pi, nous devrions

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

Le Kcombinateur est utilisé pour élever une valeur d'un certain type Aà une fonction constante sur un autre type G.

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

Le Scombinateur est utilisé pour élever des applications sur un type, dont toutes les parties peuvent dépendre.

  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 vous regardez le type de S, vous verrez qu'il énonce exactement la règle d'application contextualisée de la théorie des types, c'est donc ce qui le rend approprié pour refléter la construction d'application. C'est son travail!

Nous n'avons alors application que pour les choses fermées

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

Mais il y a un hic. J'ai écrit les types des combinateurs dans la théorie des types ordinaires, et non dans la théorie des types combinatoires. Heureusement, j'ai une machine qui fera la traduction.

Un système de type combinatoire

---------
  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

Alors voilà, dans toute sa splendeur illisible: une présentation combinatoire de Set:Set!

Il y a encore un petit problème. La syntaxe du système vous donne aucun moyen de deviner G, Aet les Bparamètres pour Set de même pour K, juste des termes. En conséquence, nous pouvons vérifier les dérivations de typage de manière algorithmique, mais nous ne pouvons pas simplement vérifier les termes du combinateur comme nous le pouvions avec le système d'origine. Ce qui pourrait fonctionner est d'exiger que l'entrée du vérificateur de type porte des annotations de type sur les utilisations de S et K, enregistrant efficacement la dérivation. Mais c'est une autre boîte de vers ...

C'est un bon endroit pour s'arrêter, si vous avez eu envie de commencer. Le reste est des trucs "en coulisses".

Génération des types de combinateurs

J'ai généré ces types combinatoires en utilisant la traduction d'abstraction entre crochets à partir des termes de la théorie des types pertinents. Pour montrer comment je l'ai fait, et rendre ce post pas totalement inutile, permettez-moi de vous proposer mon équipement.

Je peux écrire les types des combinateurs, entièrement abstraits sur leurs paramètres, comme suit. J'utilise ma pilfonction pratique , qui combine Pi et lambda pour éviter de répéter le type de domaine, et me permet plutôt utilement d'utiliser l'espace de fonctions de Haskell pour lier des variables. Peut-être que vous pouvez presque lire ce qui suit!

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)

Une fois ceux-ci définis, j'ai extrait les sous- termes ouverts pertinents et les ai exécutés tout au long de la traduction.

Une boîte à outils d'encodage de Bruijn

Voici comment construire pil. Premièrement, je définis une classe d' Finensembles ite, utilisés pour les variables. Chaque ensemble de ce type a un embedding préservant le constructeur dans l'ensemble ci-dessus, plus un nouvel topélément, et vous pouvez les distinguer: la embdfonction vous indique si une valeur est dans l'image de emb.

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

Nous pouvons, bien sûr, instancier Finpour ZeetSuc

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

Maintenant, je peux définir moins ou égal, avec une opération d' affaiblissement .

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

La wkfonction doit incorporer les éléments de xcomme les plus grands éléments de y, afin que les éléments supplémentaires ysoient plus petits, et donc en termes d'indice de Bruijn, liés plus localement.

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

Et une fois que vous avez réglé le problème, un peu de bagarre de rang n fait le reste.

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 fonction d'ordre supérieur ne vous donne pas seulement un terme représentant la variable, elle vous donne une chose surchargée qui devient la représentation correcte de la variable dans n'importe quelle portée où la variable est visible. Autrement dit, le fait que je me donne la peine de distinguer les différentes portées par type donne au vérificateur de type Haskell suffisamment d'informations pour calculer le décalage requis pour la traduction en représentation de Bruijn. Pourquoi garder un chien et aboyer?

Question 3

Je suppose que "Bracket Abstraction" fonctionne également pour les types dépendants dans certaines circonstances. Dans la section 5 de l'article suivant, vous trouverez quelques types K et S:

Coïncidences scandaleuses mais significatives
Syntaxe et évaluation de type sûr dépendant
Conor McBride, Université de Strathclyde, 2010

La conversion d'une expression lambda en une expression combinatoire correspond à peu près à la conversion d'une preuve de déduction naturelle en une preuve de style Hilbert.

Answer 1

J'ai récemment terminé un cours universitaire qui présentait Haskell et Agda (un langage de programmation fonctionnel typé dépendant), et je me demandais s'il était possible de remplacer le calcul lambda dans ces derniers par la logique combinatoire. Avec Haskell, cela semble possible en utilisant les combinateurs S et K, ce qui le rend sans point. Je me demandais quel était l'équivalent pour Agda. Par exemple, peut-on créer un langage de programmation fonctionnel typé de manière dépendante équivalent à Agda sans utiliser de variables?

En outre, est-il possible de remplacer d'une manière ou d'une autre la quantification par des combinateurs? Je ne sais pas si c'est une coïncidence mais la quantification universelle par exemple fait ressembler une signature de type à une expression lambda. Existe-t-il un moyen de supprimer la quantification universelle d'une signature de type sans changer sa signification? Par exemple dans:

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

Peut-on exprimer la même chose sans utiliser un forall?

Answer 2

21

Commencez par déterminer les types les plus dépendants possibles pour K (facile) et S (plutôt poilu). Il serait intéressant d'ajouter des constantes pour Set et Pi, puis d'essayer de reconstruire le système Set: Set de base (incohérent). Je penserais plus loin, mais j'ai un avion à prendre.

pigworker

Answer 3

J'y ai donc réfléchi un peu plus et j'ai progressé. Voici une première tentative d'encodage du système délicieusement simple (mais incohérent) de Martin-Löf Set : Setdans un style combinatoire. Ce n'est pas une bonne façon de terminer, mais c'est l'endroit le plus simple pour commencer. La syntaxe de cette théorie de type est juste un lambda-calcul avec des annotations de type, des types Pi et un ensemble d'univers.

La théorie du type de cible

Par souci d'exhaustivité, je vais présenter les règles. La validité de contexte indique simplement que vous pouvez créer des contextes à partir de vides en joignant de nouvelles variables habitant Sets.

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

Et maintenant, nous pouvons dire comment synthétiser des types pour des termes dans un contexte donné, et comment changer le type de quelque chose jusqu'au comportement de calcul des termes qu'il contient.

  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

Dans une petite variante de l'original, j'ai fait de lambda le seul opérateur de liaison, donc le deuxième argument de Pi devrait être une fonction calculant la façon dont le type de retour dépend de l'entrée. Par convention (par exemple dans Agda, mais malheureusement pas dans Haskell), la portée de lambda s'étend aussi loin que possible vers la droite, vous pouvez donc souvent laisser les abstractions sans crochets quand elles sont le dernier argument d'un opérateur d'ordre supérieur: vous pouvez voir que je l'ai fait cela avec Pi. Votre type Agda (x : S) -> Tdevient Pi S \ x:S -> T.

( Digression . Les annotations de type sur lambda sont nécessaires si vous voulez être capable de synthétiser le type d'abstractions. Si vous passez à la vérification de type comme modus operandi, vous avez toujours besoin d'annotations pour vérifier un beta-redex comme (\ x -> t) s, car vous n'avez aucun moyen pour deviner les types des parties de celui de l'ensemble. Je conseille aux concepteurs modernes de vérifier les types et d'exclure les beta-redex de la syntaxe même.)

( Digression . Ce système est incohérent car il Set:Setpermet le codage d'une variété de "paradoxes de menteur". Lorsque Martin-Löf a proposé cette théorie, Girard lui a envoyé un codage de celle-ci dans son propre système U incohérent. la construction toxique la plus soignée que nous connaissons.)

Syntaxe et normalisation du combinateur

Quoi qu'il en soit, nous avons deux symboles supplémentaires, Pi et Set, donc nous pourrions peut-être gérer une traduction combinatoire avec S, K et deux symboles supplémentaires: j'ai choisi U pour l'univers et P pour le produit.

Nous pouvons maintenant définir la syntaxe combinatoire non typée (avec des 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 :.

Notez que j'ai inclus les moyens d'inclure des variables libres représentées par type adans cette syntaxe. En plus d'être un réflexe de ma part (toute syntaxe digne de ce nom est une monade libre avec des returnvariables d'intégration et >>=une substitution performante), il sera pratique de représenter des étapes intermédiaires dans le processus de conversion des termes avec liaison à leur forme combinatoire.

Voici la normalisation:

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 exercice pour le lecteur consiste à définir un type pour exactement les formes normales et à affiner les types de ces opérations.)

Représenter la théorie des types

Nous pouvons maintenant définir une syntaxe pour notre théorie des types.

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)

J'utilise une représentation d'index de Bruijn à la manière Bellegarde et Hook (telle que popularisée par Bird et Paterson). Le type Su aa un élément de plus que a, et nous l'utilisons comme type de variables libres sous un classeur, avec Zecomme variable nouvellement liée et Su xétant la représentation décalée de l'ancienne variable libre x.

Traduire les termes en combinateurs

Et avec cela fait, nous acquérons la traduction habituelle, basée sur l' abstraction des crochets .

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

Saisir les combinateurs

La traduction montre la façon dont nous utilisons les combinateurs, ce qui nous donne un indice sur ce que devraient être leurs types. Uet ne Psont que des constructeurs définis, donc, en écrivant des types non traduits et en permettant la "notation Agda" pour Pi, nous devrions

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

Le Kcombinateur est utilisé pour élever une valeur d'un certain type Aà une fonction constante sur un autre type G.

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

Le Scombinateur est utilisé pour élever des applications sur un type, dont toutes les parties peuvent dépendre.

  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 vous regardez le type de S, vous verrez qu'il énonce exactement la règle d'application contextualisée de la théorie des types, c'est donc ce qui le rend approprié pour refléter la construction d'application. C'est son travail!

Nous n'avons alors application que pour les choses fermées

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

Mais il y a un hic. J'ai écrit les types des combinateurs dans la théorie des types ordinaires, et non dans la théorie des types combinatoires. Heureusement, j'ai une machine qui fera la traduction.

Un système de type combinatoire

---------
  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

Alors voilà, dans toute sa splendeur illisible: une présentation combinatoire de Set:Set!

Il y a encore un petit problème. La syntaxe du système vous donne aucun moyen de deviner G, Aet les Bparamètres pour Set de même pour K, juste des termes. En conséquence, nous pouvons vérifier les dérivations de typage de manière algorithmique, mais nous ne pouvons pas simplement vérifier les termes du combinateur comme nous le pouvions avec le système d'origine. Ce qui pourrait fonctionner est d'exiger que l'entrée du vérificateur de type porte des annotations de type sur les utilisations de S et K, enregistrant efficacement la dérivation. Mais c'est une autre boîte de vers ...

C'est un bon endroit pour s'arrêter, si vous avez eu envie de commencer. Le reste est des trucs "en coulisses".

Génération des types de combinateurs

J'ai généré ces types combinatoires en utilisant la traduction d'abstraction entre crochets à partir des termes de la théorie des types pertinents. Pour montrer comment je l'ai fait, et rendre ce post pas totalement inutile, permettez-moi de vous proposer mon équipement.

Je peux écrire les types des combinateurs, entièrement abstraits sur leurs paramètres, comme suit. J'utilise ma pilfonction pratique , qui combine Pi et lambda pour éviter de répéter le type de domaine, et me permet plutôt utilement d'utiliser l'espace de fonctions de Haskell pour lier des variables. Peut-être que vous pouvez presque lire ce qui suit!

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)

Une fois ceux-ci définis, j'ai extrait les sous- termes ouverts pertinents et les ai exécutés tout au long de la traduction.

Une boîte à outils d'encodage de Bruijn

Voici comment construire pil. Premièrement, je définis une classe d' Finensembles ite, utilisés pour les variables. Chaque ensemble de ce type a un embedding préservant le constructeur dans l'ensemble ci-dessus, plus un nouvel topélément, et vous pouvez les distinguer: la embdfonction vous indique si une valeur est dans l'image de emb.

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

Nous pouvons, bien sûr, instancier Finpour ZeetSuc

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

Maintenant, je peux définir moins ou égal, avec une opération d' affaiblissement .

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

La wkfonction doit incorporer les éléments de xcomme les plus grands éléments de y, afin que les éléments supplémentaires ysoient plus petits, et donc en termes d'indice de Bruijn, liés plus localement.

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

Et une fois que vous avez réglé le problème, un peu de bagarre de rang n fait le reste.

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 fonction d'ordre supérieur ne vous donne pas seulement un terme représentant la variable, elle vous donne une chose surchargée qui devient la représentation correcte de la variable dans n'importe quelle portée où la variable est visible. Autrement dit, le fait que je me donne la peine de distinguer les différentes portées par type donne au vérificateur de type Haskell suffisamment d'informations pour calculer le décalage requis pour la traduction en représentation de Bruijn. Pourquoi garder un chien et aboyer?

Answer 4

cela peut être super idiot mais comment cette image change-t-elle si vous ajoutez le Fcombinateur? Fagit différemment selon son premier argument: Si Aest un atome, Met Nsont des termes et PQest un composite, alors FAMN -> Met F(PQ)MN -> NPQ. Cela ne peut pas être représenté dans le SK(I)calcul mais Kpeut être représenté par FF. Est-il possible d'étendre votre MLTT sans points avec cela?

kram1032

Answer 5

Je suis presque sûr qu'il y a un problème avec cette procédure d'abstraction entre parenthèses, en particulier la partie «combinateurs deviennent constants», qui traduit λx.c en Kc pour les combinateurs c ∈ {S, K, U, P}. Le problème est que ces combinateurs sont polymorphes et peuvent être utilisés à un type qui dépend de x; un tel type ne peut pas être conservé par cette traduction. À titre d'exemple concret, le terme λ (A : Set) → λ (a : A) → ade type (A : Set) → (a : A) → Aest traduit en S(S(KS)(KK))(KK), qui ne peut pas être utilisé dans un type où le type du deuxième argument dépend du premier argument.

Anders Kaseorg

Answer 6

Je suppose que "Bracket Abstraction" fonctionne également pour les types dépendants dans certaines circonstances. Dans la section 5 de l'article suivant, vous trouverez quelques types K et S:

Coïncidences scandaleuses mais significatives
Syntaxe et évaluation de type sûr dépendant
Conor McBride, Université de Strathclyde, 2010

La conversion d'une expression lambda en une expression combinatoire correspond à peu près à la conversion d'une preuve de déduction naturelle en une preuve de style Hilbert.

Quel est l'équivalent en logique combinatoire de la théorie des types intuitionnistes?

Réponses:

La théorie du type de cible

Syntaxe et normalisation du combinateur

Représenter la théorie des types

Traduire les termes en combinateurs

Saisir les combinateurs

Un système de type combinatoire

Génération des types de combinateurs

Une boîte à outils d'encodage de Bruijn