Qual é o equivalente lógico combinatório da teoria dos tipos intuicionista?

87

Recentemente, concluí um curso universitário que apresentava Haskell e Agda (uma linguagem de programação funcional com tipo dependente) e queria saber se seria possível substituir o cálculo lambda nestes pela lógica combinatória. Com Haskell, isso parece possível usando os combinadores S e K, tornando-o livre de pontos. Fiquei me perguntando qual seria o equivalente para Agda. Ou seja, pode-se fazer uma linguagem de programação funcional com tipo dependente equivalente a Agda sem usar nenhuma variável?

Além disso, é possível substituir de alguma forma a quantificação por combinadores? Não sei se isso é uma coincidência, mas a quantificação universal, por exemplo, faz uma assinatura de tipo parecer uma expressão lambda. Existe uma maneira de remover a quantificação universal de uma assinatura de tipo sem alterar seu significado? Por exemplo, em:

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

A mesma coisa pode ser expressa sem usar um forall?

haskell types functional-programming logic agda Grasevski
fonte
21
Comece descobrindo os tipos mais dependentes possíveis para K (fácil) e S (bastante cabeludo). Seria interessante incluir constantes para Set e Pi e, em seguida, tentar reconstruir o sistema básico (inconsistente) de Set: Set. Eu pensaria mais, mas tenho um avião para pegar.
pigworker

Respostas:

52

Então, pensei um pouco mais e fiz alguns progressos. Aqui está uma primeira tentativa de codificar o sistema deliciosamente simples (mas inconsistente) de Martin-Löf Set : Setem um estilo combinatório. Não é uma boa maneira de terminar, mas é o lugar mais fácil para começar. A sintaxe dessa teoria de tipo é apenas lambda-cálculo com anotações de tipo, tipos Pi e um conjunto de universo.

A Teoria do Tipo de Alvo

Para fins de integridade, apresentarei as regras. A validade de contexto apenas diz que você pode construir contextos a partir do vazio, juntando novas variáveis ​​que habitam Sets.

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

E agora podemos dizer como sintetizar tipos para termos em qualquer contexto dado, e como alterar o tipo de algo até o comportamento computacional dos termos que ele contém.

  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

Em uma pequena variação do original, tornei lambda o único operador de ligação, portanto, o segundo argumento de Pi deve ser uma função que calcula a maneira como o tipo de retorno depende da entrada. Por convenção (por exemplo, em Agda, mas infelizmente não em Haskell), o escopo de lambda se estende para a direita tanto quanto possível, então você pode frequentemente deixar as abstrações sem colchetes quando elas são o último argumento de um operador de ordem superior: você pode ver que eu fiz isso com Pi. Seu tipo Agda (x : S) -> Tse torna Pi S \ x:S -> T.

( Digressão . Anotações de tipo em lambda são necessárias se você quiser ser capaz de sintetizar o tipo de abstrações. Se você alternar para verificação de tipo como seu modus operandi, ainda precisará de anotações para verificar um beta-redex como (\ x -> t) s, porque você não tem como para adivinhar os tipos das partes do todo. Aconselho os designers modernos a verificar os tipos e excluir beta-redexes da própria sintaxe.)

( Digressão . Este sistema é inconsistente, pois Set:Setpermite a codificação de uma variedade de "paradoxos mentirosos". Quando Martin-Löf propôs esta teoria, Girard enviou-lhe uma codificação em seu próprio Sistema U inconsistente. O paradoxo subsequente devido a Hurkens é o a construção tóxica mais limpa que conhecemos.)

Sintaxe e normalização do combinador

De qualquer forma, temos dois símbolos extras, Pi e Set, então talvez possamos fazer uma tradução combinatória com S, K e dois símbolos extras: eu escolhi U para o universo e P para o produto.

Agora podemos definir a sintaxe combinatória não tipada (com variáveis ​​livres):

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

Observe que incluí os meios para incluir variáveis ​​livres representadas por tipo anesta sintaxe. Além de ser um reflexo de minha parte (toda sintaxe digna desse nome é uma mônada livre com returnvariáveis ​​de incorporação e >>=substituição de desempenho), será útil representar estágios intermediários no processo de conversão de termos com ligação à sua forma combinatória.

Aqui está a normalização:

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

(Um exercício para o leitor é definir um tipo exatamente para as formas normais e aprimorar os tipos dessas operações.)

Representando a Teoria do Tipo

Agora podemos definir uma sintaxe para nossa teoria 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)

Eu uso uma representação de índice de Bruijn à maneira de Bellegarde e Hook (popularizada por Bird e Paterson). O tipo Su atem mais um elemento que a, e nós o usamos como o tipo de variáveis ​​livres em um fichário, com Zecomo a variável recém-ligada e Su xsendo a representação deslocada da antiga variável livre x.

Traduzindo Termos para Combinadores

E com isso feito, adquirimos a tradução usual, baseada na abstração de colchetes .

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

Digitando os Combinadores

A tradução mostra a maneira como usamos os combinadores, o que nos dá uma boa pista sobre quais deveriam ser seus tipos. Ue Psão apenas construtores de conjuntos, então, escrevendo tipos não traduzidos e permitindo "notação Agda" para Pi, devemos ter

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

O Kcombinador é usado para elevar um valor de algum tipo Aa uma função constante sobre algum outro tipo G.

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

O Scombinador é usado para levantar aplicações sobre um tipo, do qual todas as partes podem 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)

Se você observar o tipo de S, verá que ele afirma exatamente a regra de aplicação contextualizada da teoria de tipo, de modo que é o que o torna adequado para refletir a construção do aplicativo. Esse é o seu trabalho!

Então, temos aplicação apenas para coisas fechadas

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

Mas há um obstáculo. Eu escrevi os tipos de combinadores na teoria dos tipos comuns, não na teoria dos tipos combinatórios. Felizmente, tenho uma máquina que fará a tradução.

Um sistema de tipo combinatório

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

Então aí está, em toda a sua glória ilegível: uma apresentação combinatória de Set:Set!

Ainda há um pequeno problema. A sintaxe do sistema não oferece nenhuma maneira de adivinhar os parâmetros G, Ae Bpara Se de forma semelhante K, apenas a partir dos termos. Da mesma forma, podemos verificar as derivações de tipagem algoritmicamente, mas não podemos simplesmente verificar os termos do combinador como poderíamos com o sistema original. O que pode funcionar é exigir que a entrada para o verificador de tipo tenha anotações de tipo sobre os usos de S e K, registrando efetivamente a derivação. Mas essa é outra lata de vermes ...

Este é um bom lugar para parar, se você estiver interessado em começar. O resto é coisa de "bastidores".

Gerando os Tipos de Combinadores

Eu gerei esses tipos combinatórios usando a tradução de abstração de colchetes dos termos relevantes da teoria de tipo. Para mostrar como fiz isso, e tornar este post não totalmente inútil, deixe-me oferecer meu equipamento.

Posso escrever os tipos de combinadores, totalmente abstraídos de seus parâmetros, como segue. Eu uso minha pilfunção prática , que combina Pi e lambda para evitar a repetição do tipo de domínio e, de forma bastante útil, me permite usar o espaço de funções de Haskell para vincular variáveis. Talvez você quase possa ler o seguinte!

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)

Com eles definidos, extraí os subtermos abertos relevantes e os executei na tradução.

A de Bruijn Encoding Toolkit

Veja como construir pil. Em primeiro lugar, defino uma classe de Finconjuntos de itens, usados ​​para variáveis. Cada um desses conjuntos tem um embedding que preserva o construtor no conjunto acima, além de um novo topelemento, e você pode diferenciá-los: a embdfunção informa se um valor está na imagem de emb.

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

Podemos, é claro, instanciar Finpara ZeeSuc

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

Agora posso definir menos ou igual, com uma operação de enfraquecimento .

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

A wkfunção deve incorporar os elementos de xcomo os maiores elementos de y, de modo que as coisas extras em ysejam menores e, portanto, em termos de índice de de Bruijn, limitados mais 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

E uma vez que você tenha resolvido isso, um pouco de malandragem faz o 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)

A função de ordem superior não fornece apenas um termo que representa a variável, mas também uma coisa sobrecarregada que se torna a representação correta da variável em qualquer escopo onde a variável esteja visível. Ou seja, o fato de que me dou ao trabalho de distinguir os diferentes escopos por tipo dá ao inspetor de tipos Haskell informações suficientes para calcular o deslocamento necessário para a tradução para a representação de Bruijn. Por que ter um cachorro e latir sozinho?

trabalhador de porco
fonte
isso pode ser muito bobo, mas como essa imagem muda se você adicionar o Fcombinador? Fage de forma diferente dependendo de seu primeiro argumento: Se Aé um átomo, Me Nsão termos e PQé um composto, então FAMN -> Me F(PQ)MN -> NPQ. Isso não pode ser representado em SK(I)cálculo, mas Kpode ser representado como FF. É possível estender seu ponto MLTT grátis com isso?
kram1032
Tenho certeza de que há um problema com esse procedimento de abstração de colchetes, especificamente a parte “combinadores tornam-se constantes”, que traduz λx.c para Kc para os combinadores c ∈ {S, K, U, P}. O problema é que esses combinadores são polimórficos e podem ser usados ​​em um tipo que depende de x; tal tipo não pode ser preservado por esta tradução. Como um exemplo concreto, o termo λ (A : Set) → λ (a : A) → ade tipo (A : Set) → (a : A) → Aé traduzido para S(S(KS)(KK))(KK), que não pode ser usado em um tipo em que o tipo do segundo argumento depende do primeiro argumento.
Anders Kaseorg
8

Acho que a "Abstração de colchetes" também funciona para tipos dependentes em algumas circunstâncias. Na seção 5 do seguinte artigo, você encontrará alguns tipos K e S:

Coincidências ultrajantes, mas significativas
Sintaxe e avaliação de tipo seguro dependente
Conor McBride, University of Strathclyde, 2010

Converter uma expressão lambda em uma expressão combinatória corresponde aproximadamente a converter uma prova de dedução natural em uma prova de estilo de Hilbert.

Mostowski Collapse
fonte