Tipos universais e existenciais

9

Estou tentando entender os conceitos de tipos existenciais e universais, mas em todos os lugares que vejo, vejo intuições ou implementações lógicas ou operacionais (por exemplo, livro TAPL de B. Pierce), o que, bem ... é bom , mas gostaria de ver as definições (onde as vemos como conjuntos) - e a partir delas, derivações de algumas leis, bem como justificativas para nossas intuições.

Portanto, como não consigo encontrar essas definições, decidi fazer isso sozinho e acho que estas podem ser razoáveis:

x.T:=defStypeT[x:=S]
x.T:=defStypeT[x:=S]

Mas, no mencionado livro TAPL, recebemos essa definição (embora eu a chamasse de identidade)

x.T:=defy.(x.Ty)y()

Eu tenho dois problemas com isso:

  1. No LHS de eu esperaria que fosse a única variável livre de (porque como visualizar um tipo "ainda não construído" com algumas variáveis ​​livres penduradas nele?), Mas no RHS parece que pode ter algum impacto sobre , então é melhor que seja uma variável livre em . Portanto, o LHS não pode ser igual ao RHS porque conjuntos de variáveis ​​livres de diferem nos dois lados, certo?()xTyTTT
  2. Mesmo desconsiderando a preocupação no ponto 1. - Tentei reescrever o RHS usando minhas definições e ver se consigo obter minha definição de tipo existencial, mas fiquei preso:
    RHS=S(x.Ty)[y:=S]S=S(RT[x:=R,y:=S]S)S

Nem lembra remotamente minha definição. É possível simplificar a fórmula que cheguei? Intuitivamente, porque existem tipos de função, provavelmente nunca será igual à minha definição. Mas se eles não são iguais - são pelo menos 'isomórficos' em algum sentido? Se não - o que "deu errado"?

pesado
fonte
1
Há um erro de digitação na sua equação (*): deve ser vez de . yYy
Cody
1
Além disso, em sua última equação: pode não aparecer em ! TyT
Cody

Respostas:

9

A teoria dos conjuntos está prejudicando você aqui e, quanto mais cedo você se libertar dela, melhor será para a sua compreensão da ciência da computação.

Esqueça as interseções e uniões. As pessoas têm a idéia de que e são como e , que é o tipo de coisa que a escola polonesa fazia há muito tempo com álgebras booleanas, mas realmente não é o caminho a seguir (definitivamente não no computador Ciência).

Você gostaria de vê-los como conjuntos. Ok, mas precisamos ignorar questões de tamanho e fingir que existe um conjunto de todos os conjuntos. (É possível corrigir os problemas de tamanho passando para uma categoria diferente.) O tipo é realmente como o produto cartesiano Ou seja, um elemento de é uma função de conjuntos para conjuntos: para cada conjunto , fornece um elemento do tipo . Por exemplo, um elemento de é uma função que recebe um conjuntoX . T : = Π S : S e T T [ X S ] . X . T f S f ( S ( S S ) f 0 ( S ) ( g ) ( x ) : = x f 1 ( S ) ( g ) ( x)x.T

X.T:=S:SetT[XS].
X.T fST [ x S ] X . ( X X ) ( X X ) f S ( S S ) f(S)T[xS]X.(XX)(XX)fSe fornece uma função do tipo . Aqui estão algumas funções: Portanto, obtemos um para cada número natural e é meio difícil pensar em outros exemplos . (Exercício: google "Codificação da Igreja de números naturais".)(SS)(SS)
f0(S)(g)(x):=xf1(S)(g)(x):=g(x)f2(S)(g)(x):=g(g(x))f3(S)(g)(x):=g(g(g(x)))

A seguir, vejamos os tipos existenciais. Em primeiro lugar, a codificação correta de em termos de é onde a variável não aparece em ! (Isso deve ser mencionado no TAPL de Pierce.) Antes de examinarmos essa codificação, vamos fazer diretamente em termos de conjuntos. Desta vez, é um coproduto: Um elemento de é um par onde é um conjunto e é um elemento deX . T : =Y . ( X . ( T Y ) ) Y Y TX . T X . T : = S : S e T T [ X S ] . X . T ( S , a ) S a T [

X.T:=Y.(X.(TY))Y
YTX.T
X.T:=S:SetT[XS].
X.T (S,a)SaT[XS] . Um exemplo seria o tipo , cujos elementos são pares onde é um conjunto e é uma operação binária nele. Isso também é conhecido como magma . Se você fica um pouco mais extravagante, pode expressar estruturas conhecidas, como grupos e anéis (é necessário inventar tipos de identidade primeiro).( S , m ) S m : S × S SX.(X×XX)(S,m)Sm:S×SS

Vamos ver como a codificação de em termos de funciona. É errado esperar que obteremos uma igualdade entre e (NB: é recente) - apenas a teoria dos conjuntos daria às pessoas tais expectativas. Deveríamos esperar que os dois fossem isomórficos . Portanto, a tarefa é encontrar uma bijeção entre e Este é um exercício emX.TY.(X.(TY))YY

A:=S:SetT[XS]
B:=R:Set(S:Set(T[XS]R))R.
λ-cálculo. Em uma direção, temos o mapa definido como e na outra um mapa definido por (A notação significa a função .) Agora podemos verificar se e são inversos um do outro. Uma direção é fácil: A outra direção fica assim: f:AB
f(S,a)(R)(h):=h(S)(a)
g:BA
g(ϕ):=ϕ(A)(λS.λa.(S,a)).
λS.λa.(S,a)Sa(S,a)fg
g(f(S,a))=f(S,a)(A)(λS.λa.(S,a))=(λS.λa.(S,a)(S)(a)=(S,a).
f(g(ϕ))(R)(h)=h(π1(g(ϕ))(π2(g(ϕ))).
Poderíamos continuar reescrevendo para , mas ficaríamos presos!g(ϕ)ϕ(A)(λS.λa.(S,a))

Acontece que na teoria dos conjuntos a codificação de em termos de faz não trabalho. Mas funciona em outras configurações, onde tipos não são conjuntos. Por exemplo, você pode se convencer de que na lógica as declarações é equivalente a que varia sobre todas as proposições (valores de verdade, declarações lógicas). Novamente, a variável não deve ocorrer em .

x.ϕ(x)
P:Prop.(x.(ϕ(x)P))P,
PPϕ
Andrej Bauer
fonte
1
Andrej, você é tão rápido quanto um raio!
Cody
Isso é esclarecedor, obrigado! Mas ainda tenho dúvidas :) 1) entendo corretamente, que a configuração que você apresentou ainda é teórica (mas não tão ingênua quanto a minha) e é por isso que não se sustenta e não temos esperanças de achar apropriado e ? 2) Entendo que na lógica essas declarações são equivalentes, mas parece-me que escapa um pouco da teoria dos tipos (bem, porque onde estão os tipos? :)). Então, qual seria a configuração do sistema de tipos no qual é válido? 3) se estou implementando uma linguagem baseada no cálculo lambda - devo tomar cuidado ao usar ? ()fg()()
socumbersome
3
Correto: o "modelo" set-teórica (que é não um modelo, porque nós fingimos que nós podemos fazer produtos cartesianos indexados por todos os conjuntos) viola a codificação de em termos de . A teoria de tipos também não valida a codificação. Em vez disso, dá-lhe uma retração (basta usar a mesma e acima para a teoria tipo), mas não um isomorfismo. Para obter um isomorfismo, você precisa de algo extra, por exemplo, a parametricidade garante que todos os elementos do produto cartesiano sejam bem comportados e recupere o isomorfismo. fg
Andrej Bauer
@AndrejBauer é o sistema subjacente impredicativo? E, no caso de uma resposta positiva, o isomorfismo vale para sistemas predicativos?
Giorgio Mossa
@GiorgioMossa: qual sistema? Você está perguntando se é necessário impredicatividade para estabelecer a validade da codificação de em termos de ? Não, a parametridade é suficiente, embora às vezes a impredicatividade ajude (por exemplo, quando expressamos usando ni a topos).
Andrej Bauer
3

Em relação à questão 1): a variável não deve aparecer em ; de fato, ela precisa ser irrestrita. Se você quiser ter alguma esperança dos lhs sendo igual à rhs, certamente você deve ter o mesmo número de variáveis livres de cada lado, que é impossível se é capturado em . A intuição é que deve ser igual à conjunção infinita para todo tipo possível . De fato, não é difícil mostrar para qualquer tipo específico queY Y T T ( ( x . T U 0 ) U 0 ) ( ( x . T U 1 ) U 1 ) Y YYTT

((x.TU0)U0)((x.TU1)U1)
UiU
x.T((x.TU)U)

Em palavras:

Provando que, se existe algum (arbitrário) tal que é válido, então é igual a provar que, para qualquer , se é válido, .xT(x)U xT(x)U

Note que não deve depender de .Ux

A intuição por trás da igualdade é que esse fato, para todo possível,U é suficiente para caracterizar o quantificador existencial.

Para 2), a intuição teórica dos conjuntos é um pouco difícil aqui, receio. Não é ingenuamente possível pensar nos tipos como conjuntos de elementos e setas como as funções da teoria dos conjuntos entre eles. No entanto, intuitivamente, se alguma interseção não estiver vazia, deverá estar não vazia. No seu caso, isso fornece SA(S)A()

(R(T[x:=R]))

(observe o parêntese) que precisa estar vazio. Mas a única maneira para isso é que exista um tal que esteja vazio, o que significa que precisa estar vazio.T [ x : = R ] T [ x : = R ]RT[x:=R]T[x:=R]

cody
fonte
1
Não! Não é uma conjunção infinita. É um produto infinito . A conjunção esquece o que aconteceu em cada tipo e isso é desagradável. (Não vamos contar a ninguém que nos modelos que capacidade de realização de sistema F o quantificador universal é interseção.)Ui
Andrej Bauer
@AndrejBauer: isso é justo, embora às vezes seja útil esquecer as informações ... minha intuição é parcialmente baseada na regra de eliminação de .
Cody
Você só pode esquecer as informações em circunstâncias adequadas que garantam que você continuará impune. Por exemplo, nos modelos de realizabilidade onde realmente é , podemos esquecer as informações devido à incrível quantidade de uniformidade dos realizadores. Se você esquecer as informações quando não deveria fazê-las, apenas invalidará as leis.
Andrej Bauer
1

Sugiro não desistir da intuição operacional. Operacional é primário, todas as semânticas são derivadas e são apenas técnicas de prova para semântica operacional. As idéias principais são as seguintes.

Um programa usa uma variável universal-polimorficamente , desde que não faça nada com que exija conhecimento do tipo de . Por exemplo, no -calculus, as seguintes operações podem ser polimórficas (se são ou não, depende da semântica precisa da linguagem).Px Pxxλ

  • encaminhamento, por exemplo, ,λx.x.
  • reordenação, por exemplo, .λ(x,y,z).(z,x,y)
  • duplicação, por exemplo, .λx.(x,x)
  • caindo, por exemplo, .λx.7

Agora, o polimofismo existencial é o exato dual do polimorfismo universal: um programa usa uma variável existencial-polimofialmente , se fornece somente para contextos que não exigem conhecimento do tipo de . Em outras palavras, fornece somente para contextos que usam polimorficamente universal.xPx x x P x xPxxPxx

Na minha opinião, essa bela simetria é obscurecida quando se pensa em polimorfismo universal / existencial no . O motivo é a forte dependência do operador do espaço de funções que, infelizmente, não é realmente um operador dualizador, mas algo mais complicado (covariante em um argumento, contravariante no outro).λ

Martin Berger
fonte
Um ponto de vista interessante (embora eu não o entenda totalmente :)). A idéia é verificar se as leis derivadas dessa visão geral se mantêm em configurações concretas de sistemas de tipos? E onde posso encontrar algum texto introdutório sobre isso?
socumbersome
@socumbersome A maioria das implementações existentes de polimorfismo não entendem isso direito. De fato, a quantificação existencial raramente é implementada diretamente. Receio que não haja texto introdutório descrevendo a dualidade. Nós explicamos aqui, mas foi escrito para um público especializado.
Martin Berger