Tipos universais e existenciais

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:

\forall x . T \overset{d e f}{:=} ⋂_{S - t y p e} T [x := S]

$\forall x.T \overset{def}{:=} \bigcap_{S - type} T[x := S]$

\exists x . T \overset{d e f}{:=} ⋃_{S - t y p e} T [x := S]

$\exists x.T \overset{def}{:=} \bigcup_{S - type} T[x := S]$

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

\exists x . T \overset{d e f}{:=} \forall y . (\forall x . T \to y) \to y (*)

$\exists x.T \overset{def}{:=} \forall y. (\forall x. T \rightarrow y) \rightarrow y \quad (*)$

Eu tenho dois problemas com isso:

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? $(*)$ $x$ $T$ $y$ $T$ $T$ $T$
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: $R H S = ⋂_{S} (\forall x . T \to y) [y := S] \to S = ⋂_{S} (⋂_{R} T [x := R, y := S] \to S) \to S$ $RHS = \bigcap_{S} (\forall x.T \rightarrow y)[y := S] \rightarrow S = \bigcap_{S} \left(\bigcap_{R} T[x := R, y := S] \rightarrow S\right) \rightarrow 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"?

lo.logic type-theory type-systems set-theory pesado
fonte

Há um erro de digitação na sua equação (*): deve ser vez de .

\forall Y

$\forall Y$

\forall y

$\forall y$

Cody

Além disso, em sua última equação: pode não aparecer em !

y

$y$

T

$T$

Cody

Respostas:

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). $\forall$ $\exists$ $\bigcap$ $\bigcup$

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 conjunto $\forall x . T$

\forall X . T : = \prod_{S : S e t} T [X \mapsto S] .

$\forall X . T \mathrel{{:}{=}} \prod_{S : \mathsf{Set}} T[X \mapsto S].$

\forall X . T

$\forall X . T$

f

$f$

S

$S$

f (S)

$f(S)$

T [x \mapsto S]

$T[x \mapsto S]$

\forall X . (X \to X) \to (X \to X)

$\forall X. (X \to X) \to (X \to X)$

f

$f$

S

$S$ e 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".)

(S \to S) \to (S \to S)

$(S \to S) \to (S \to S)$

\begin{aligned} f_{0} (S) (g) (x) & : = x \\ f_{1} (S) (g) (x) & : = g (x) \\ f_{2} (S) (g) (x) & : = g (g (x)) \\ f_{3} (S) (g) (x) & : = g (g (g (x))) \end{aligned}

$\begin{align*} f_0(S)(g)(x) &\mathrel{{:}{=}} x \\ f_1(S)(g)(x) &\mathrel{{:}{=}} g(x) \\ f_2(S)(g)(x) &\mathrel{{:}{=}} g(g(x)) \\ f_3(S)(g)(x) &\mathrel{{:}{=}} g(g(g(x))) \end{align*}$

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 de $\exists$ $\forall$

\exists X . T : = \forall Y . (\forall X . (T \to Y)) \to Y

$\exists X . T \mathrel{{:}{=}} \forall Y . (\forall X . (T \to Y)) \to Y$ $Y$ $T$

\exists X . T

$\exists X . T$

\exists X . T : = \underset{S : S e t}{∐} T [X \mapsto S] .

$\exists X . T \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S].$

\exists X . T

$\exists X . T$

(S, a)

$(S, a)$

S

$S$

a

$a$

T [X \mapsto S]

$T[X \mapsto S]$ . 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).

\exists X . (X \times X \to X)

$\exists X . (X \times X \to X)$

(S, m)

$(S, m)$

S

$S$

m : S \times S \to S

$m : S \times S \to S$

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 em $\exists$ $\forall$ $\exists X. T$ $\forall Y . (\forall X . (T \to Y)) \to Y$ $Y$

A : = \underset{S : S e t}{∐} T [X \mapsto S]

$A \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S]$

B : = \prod_{R : S e t} (\prod_{S : S e t} (T [X \mapsto S] \to R)) \to R .

$B \mathrel{{:}{=}} \prod_{R : \mathsf{Set}} \left(\prod_{S : \mathsf{Set}} (T[X \mapsto S] \to R) \right) \to R.$

λ

$\lambda$ -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 : A \to B

$f : A \to B$

f (S, a) (R) (h) : = h (S) (a)

$f(S,a)(R)(h) \mathrel{{:}{=}} h(S)(a)$

g : B \to A

$g : B \to A$

g (ϕ) : = ϕ (A) (λ S . λ a . (S, a)) .

$g(\phi) \mathrel{{:}{=}} \phi(A)(\lambda S . \lambda a . (S, a)).$

λ S . λ a . (S, a)

$\lambda S . \lambda a . (S, a)$

S \mapsto a \mapsto (S, a)

$S \mapsto a \mapsto (S, a)$

f

$f$

g

$g$

g (f (S, a)) = f (S, a) (A) (λ S^{'} . λ a^{'} . (S^{'}, a^{'})) = (λ S^{'} . λ a^{'} . (S^{'}, a^{'}) (S) (a) = (S, a) .

$g(f(S,a)) = f(S,a)(A)(\lambda S' . \lambda a' . (S', a')) = (\lambda S' . \lambda a' . (S', a')(S)(a) = (S, a).$

f (g (ϕ)) (R) (h) = h (π_{1} (g (ϕ)) (π_{2} (g (ϕ))) .

$f(g(\phi))(R)(h) = h(\pi_1(g(\phi))(\pi_2(g(\phi))).$ Poderíamos continuar reescrevendo para , mas ficaríamos presos!

g (ϕ)

$g(\phi)$

ϕ (A) (λ S . λ a . (S, a))

$\phi(A)(\lambda S . \lambda 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 . $\exists$ $\forall$

\exists x . ϕ (x)

$\exists x . \phi(x)$

\forall P : P r o p . (\forall x . (ϕ (x) \Rightarrow P)) \Rightarrow P,

$\forall{P : \mathsf{Prop}} . (\forall x . (\phi(x) \Rightarrow P)) \Rightarrow P,$

P

$P$

P

$P$

ϕ

$\phi$

Andrej Bauer
fonte

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 ?

(*)

$(*)$

f

$f$

g

$g$

(*)

$(*)$

(*)

$(*)$

socumbersome

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.

\exists

$\exists$

\forall

$\forall$

f

$f$

g

$g$

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

\exists

$\exists$

\forall

$\forall$

\exists

$\exists$

\forall

$\forall$

Andrej Bauer

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 que $Y$ $Y$ $Y$ $T$ $\exists T$

((\forall x . T \to U_{0}) \to U_{0}) \land ((\forall x . T \to U_{1}) \to U_{1}) \land \dots

$((\forall x. T\rightarrow U_0)\rightarrow U_0)\wedge((\forall x. T\rightarrow U_1)\rightarrow U_1)\wedge\ldots$

U_{i}

$U_i$

U

$U$

\exists x . T \to ((\forall x . T \to U) \to U)

$\exists x.T \rightarrow ((\forall x. T\rightarrow U)\rightarrow 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, . $x$ $T(x)$ $U$ $x$ $T(x)$ $U$

Note que não deve depender de . $U$ $x$

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 $\bigcap_S A(S)$ $A(\varnothing)$

(⋂_{R} (T [x := R] \to \emptyset)) \to \emptyset

$\left(\bigcap_R \left(T[x:=R]\rightarrow \varnothing\right)\right)\rightarrow\varnothing$

(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. $R$ $T[x:=R]\rightarrow \varnothing$ $T[x:=R]$

cody
fonte

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

U_{i}

$U_i$

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 .

\exists

$\exists$

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.

\forall

$\forall$

⋂

$\bigcap$

Andrej Bauer

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). $P$ $x$ $P$ $x$ $x$ $\lambda$

encaminhamento, por exemplo, , $\lambda x.x.$
reordenação, por exemplo, . $\lambda (x,y,z). (z,x, y)$
duplicação, por exemplo, . $\lambda x.(x,x)$
caindo, por exemplo, . $\lambda 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. $P$ $x$ $P$ $x$ $x$ $P$ $x$ $x$

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). $\lambda$

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