Por que Coq tem Prop?

35

A Coq tem um tipo Prop de proposições irrelevantes à prova que são descartadas durante a extração. Quais são as razões para isso, se usarmos o Coq apenas para provas. Prop é impredicativo, portanto Prop: Prop, no entanto, Coq infere automaticamente os índices do universo e podemos usar o Tipo (i) em qualquer lugar. Parece que Prop complica muito tudo.

Eu li que existem razões filosóficas para separar Set e Prop no livro de Luo, no entanto, não as encontrei no livro. O que eles são?

Konstantin Solomatov
fonte
6
“Se usarmos o Coq apenas para provas”: acho que você identificou um ponto-chave aqui. Coq não é usado apenas para provas.
Gilles 'SO- stop be evil'

Respostas:

34

k k k P r o pProp é muito útil para a extração de programas, pois permite excluir partes do código que são inúteis. Por exemplo, para extrair um algoritmo de classificação, provaríamos a afirmação "para cada lista existe uma lista tal que é ordenado e é uma permutação de ". Se escrevermos isso em Coq e extraímos sem usar , obteremos:kkkProp

  1. "para todos existe " nos dará um mapa que leva listas para listas,kksort
  2. "tal que seja ordenado" fornecerá uma função que percorre e verifica se está classificada, ekkverifyk
  3. " é uma permutação de " dará uma permutação que leva a . Observe que não é apenas um mapeamento, mas também o mapeamento inverso, juntamente com programas que verificam se os dois mapas são realmente inversos.kkpikpi

Embora o material extra não seja totalmente inútil, em muitos aplicativos queremos nos livrar dele e ficar justos sort. Isso pode ser feito se usarmos para declarar " está ordenado" e " é uma permutação de ", mas não "para todos há ". k k kPropkkk

Em geral, uma maneira comum de extrair código é considerar uma declaração no formato que é inserido, é saída e explica o que significa para ser uma saída correta. (No exemplo acima, e são os tipos de lista e é " é ordenado e é uma permutação de .") Se estiver em então extração dá um mapa tal que vale para todosx y ϕ ( x , y ) y A B ϕ ( , k ) k k ϕ P r o p f : A B ϕ ( x , f ( x ) ) x A ϕ S e t g g ( x ) ϕ ( x ,x:A.y:B.ϕ(x,y)xyϕ(x,y)yABϕ(,k)kkϕPropf:ABϕ(x,f(x))xA . Se é em então nós também terá uma função tal que é a prova de que detém, para todos . Muitas vezes, a prova é computacionalmente inútil e preferimos nos livrar dela, especialmente quando está aninhada profundamente em alguma outra declaração. nos dá a possibilidade de fazer isso.ϕSetgg(x)x A P r o pϕ(x,f(x))xAProp

Adicionado em 29/07/2015: Há uma dúvida sobre se poderíamos evitar ao otimizar automaticamente "código inútil extraído". Até certo ponto, podemos fazer isso, por exemplo, todo o código extraído do fragmento negativo da lógica (coisas criadas a partir do tipo vazio, tipo de unidade, produtos) é inútil, pois apenas embaralha a unidade. Mas existem decisões de design genuínas que você precisa tomar ao usar . Aqui está um exemplo simpe, onde significa que estamos em e significa que estamos em . Se extrairmos de P r o p Σ T y p eP r o p Π n : N Σ b : { 0 , 1 } Σ k : NPropPropΣTypePropn b k Π N : N Σ b : { 0 , 1 }K : N

Πn:NΣb:{0,1}Σk:Nn=2k+b
obteremos um programa que decompõe em seu bit mais baixo os bits restantes , ou seja, ele calcula tudo. Se extrairmos de , o programa calculará apenas o bit mais baixo . A máquina não sabe qual é a correta, o usuário precisa dizer o que deseja.nbkb
Πn:NΣb:{0,1}k:Nn=2k+b
b
Andrej Bauer
fonte
11
Estou um pouco confuso. Você está dizendo que sem seria impossível reconhecer no programa extraído que não contribui para a saída (isto é, que apenas a verifica)? Existem cenários em que não seria possível extrair esse código inútil pelos meios usuais disponíveis para os otimizadores de código? g ( x )Propg(x)
usuário
11
No programa extraído, pode-se dizer "quero " e voltar a partir daí. Não consegui criar um cenário tão enredado que não pudéssemos otimizar nada que não contribuísse diretamente para determinar a permutação sem que fosse realmente necessário computar essa permutação (de qualquer maneira, do ponto de vista da otimização global) ) k
usuário
11
Você não tem a informação "Eu quero ". Essa é uma suposição extra e, obviamente, uma vez que eles dizem qual resultado específico eles desejam, você pode simplesmente otimizar o código morto. Na verdade, pensei em uma resposta melhor: é uma questão de design que itens colocar em . Você precisa saber o que o usuário deseja, e ele informa o que deseja usando . É fácil criar exemplos em que existem várias opções. Vou adicionar um à minha resposta. P r o p P r o pkPropProp
Andrej Bauer
2
(1)
3
Prop
19

Prop

impredicative Prop+large elimination+excluded middle

é inconsistente. Normalmente, você deseja manter a possibilidade de adicionar o meio excluído, portanto, uma solução é manter uma grande eliminação e tornar o Prop predicativo. O outro é suprimir grande eliminação.

Coq fez os dois! Eles renomearam o predicativo Prop to Set e desativaram grande eliminação no Prop.

A expressividade obtida pela impredicatividade é "tranquilizadora", no sentido em que 99% da matemática "razoável" pode ser formalizada com ela, e sabe-se que ela é consistente em relação à teoria dos conjuntos. Isso torna provável que eles não o enfraquecem para algo como o Agda, que possui apenas universos predicativos.

cody
fonte
8
Ah, e esqueci de mencionar: não é esse o caso Prop : Prop, isso seria inconsistente. Em vez disso, quantificações sobre todas as proposições são novamente uma proposição.
Cody
Você poderia me indicar mais recursos sobre isso? Tudo o que encontro parece muito disperso.
user833970
11
@ user833970 alguma coisa específica que você gostaria de apontar? Receio que não haja realmente uma referência abrangente para a meta-teoria dos tipos dependentes. Esta discussão (que aponta aqui!) Pode ser útil: github.com/FStarLang/FStar/issues/360
cody
obrigado, estou trabalhando no artigo do paradoxo da Berardi agora, acho que isso esclarecerá minha confusão.
user833970
14

Mesmo que você não esteja interessado em extrair programas, o fato de Propser impredicativo permite criar alguns modelos que não podem ser construídos usando uma torre predicativa de universos. O IIRC Thorsten Altenkirch tem um modelo do Sistema F usando a impredicatividade da Coq.

Gallais
fonte