Diz-se que o CoC é o culminar de todas as três dimensões do cubo Lambda. Isso não é aparente para mim. Acho que entendo as dimensões individuais, e a combinação de duas parece resultar em uma união relativamente direta (talvez esteja faltando alguma coisa?). Mas quando olho para o CoC, em vez de parecer uma combinação dos três, parece uma coisa completamente diferente. De qual dimensão Tipo, Prop e tipos pequeno / grande vêm? Para onde desapareceram os produtos dependentes? E por que há um foco em proposições e provas em vez de tipos e programas? Existe algo equivalente focado em tipos e programas?
Edit: Caso não esteja claro, estou pedindo uma explicação de como o CoC é equivalente à união direta das dimensões do cubo Lambda. E existe uma união real dos três por aí em algum lugar que eu possa estudar (ou seja, em termos de programas e tipos, não de provas e proposições)? Isso é uma resposta a comentários sobre a pergunta, não a respostas atuais.
soft-question
. Não vejo uma pergunta técnica aqui. Talvez você possa ser um pouco mais específico quanto ao que está perguntando?Respostas:
Primeiro, para reiterar um dos pontos de Cody, o Cálculo de Construções Indutivas (no qual o núcleo de Coq se baseia) é muito diferente do Cálculo de Construções. É melhor pensar em começar na teoria de tipos de Martin-Löf com universos e, em seguida, adicionar um tipo Prop na parte inferior da hierarquia de tipos. Este é um animal muito diferente do CoC original, que é melhor pensado como uma versão dependente do F-ômega. (Por exemplo, a CiC possui modelos teóricos e o CoC não.)
Dito isto, o cubo lambda (do qual o CoC é membro) é normalmente apresentado como um sistema de tipo puro por razões de economia no número de regras de digitação. Ao tratar tipos, tipos e termos como elementos da mesma categoria sintática, você pode escrever muito menos regras e suas provas também ficam um pouco menos redundantes.
No entanto, para entender, pode ser útil separar as diferentes categorias explicitamente. Podemos introduzir três categorias sintáticas, tipos (variados pelo metavariável
k
), tipos (variados pelo metavariávelA
) e termos (variados pelo metavariávele
). Todos os oito sistemas podem ser entendidos como variações do que é permitido em cada um dos três níveis.λ → (cálculo lambda de digitação simples)
Este é o cálculo lambda básico digitado. Existe um único tipo
∗
, que é o tipo de tipos. Os próprios tipos são tipos atômicosp
e tipos de funçãoA → B
. Termos são variáveis, abstrações ou aplicativos.λω_ (STLC + operadores do tipo superior)
O STLC permite apenas abstração no nível dos termos. Se o adicionarmos no nível dos tipos, adicionaremos um novo tipo,
k → k
que é o tipo de funções no nível do tipo, e abstraçãoλa:k.A
e aplicaçãoA B
no nível do tipo. Então agora não temos polimorfismo, mas temos operadores de tipo.Se a memória servir, este sistema não terá mais poder computacional que o STLC; apenas oferece a capacidade de abreviar tipos.
λ2 (Sistema F)
Em vez de adicionar operadores de tipo, poderíamos ter adicionado polimorfismo. No nível de tipo, adicionamos
∀a:k. A
qual é um antigo tipo polimórfico e, no nível de termo, adicionamos abstração sobre tiposΛa:k. e
e aplicação de tipoe [A]
.Este sistema é muito mais poderoso que o STLC - é tão forte quanto a aritmética de segunda ordem.
λω (Sistema F-ômega)
Se tivermos operadores de tipo e polimorfismo, obteremos o F-ômega. Este sistema é mais ou menos a teoria do tipo de kernel da maioria das linguagens funcionais modernas (como ML e Haskell). Também é muito mais poderoso que o Sistema F - é equivalente em força à aritmética de ordem superior.
λP (LF)
Em vez de polimorfismo, poderíamos ter ido na direção da dependência do cálculo lambda de tipo simples. Se você permitiu que o tipo de função deixasse seu argumento ser usado no tipo de retorno (ou seja, escreva em
Πx:A. B(x)
vez deA → B
), você obtém λP. Para tornar isso realmente útil, precisamos estender o conjunto de tipos com um tipo de operador de tipo que aceita termos como argumentosΠx:A. k
e, portanto, precisamos adicionar uma abstraçãoΛx:A.B
e aplicação correspondentesA [e]
no nível de tipo.Às vezes, esse sistema é chamado LF, ou Edinburgh Logical Framework.
Ele tem a mesma força computacional do cálculo lambda de tipo simples.
λP2 (sem nome especial)
Também podemos adicionar polimorfismo a λP, para obter λP2. Este sistema não é usado com frequência, portanto, não possui um nome específico. (O artigo que li que a utilizou é a indução de Herman Geuvers não é derivável na teoria de tipos dependentes de segunda ordem .)
Este sistema tem a mesma força que o sistema F.
λPω_ (sem nome especial)
Também poderíamos adicionar operadores de tipo a λP, para obter λPω_. Isso envolve adicionar um tipo
Πa:k. k'
para operadores de tipo e abstraçãoΛx:A.B
e aplicativo de nível de tipo correspondenteA [e]
.Como novamente não há salto na força computacional sobre o STLC, esse sistema também deve ser uma boa base para uma estrutura lógica, mas ninguém conseguiu.
λPω (o cálculo de construções)
Finalmente, chegamos ao λPω, o Cálculo de Construções, pegando λPω_ e adicionando uma abstração do tipo polimórfico
∀a:k.A
e uma abstração em nível de termoΛa:k. e
e aplicaçãoe [A]
para ele.Os tipos desse sistema são muito mais expressivos que no F-ômega, mas têm a mesma força computacional.
fonte
Eu sempre quis tentar resumir cada dimensão do cubo- e o que eles representam, então vou dar uma chance a este.λ
Mas, primeiro, deve-se tentar desembaraçar várias questões. O provador de teoremas interativos da Coq é baseado em uma teoria de tipos subjacente, às vezes chamada amorosamente de cálculo de construções indutivas com universos . Você notará que isso é mais emocionante do que simplesmente "Cálculo de Construções" e, de fato, há muito mais coisas além do CoC. Em particular, acho que você está confuso sobre exatamente quais recursos estão em CoC apropriados. Em particular, a distinção Set / Prop e universos não aparecem no CoC.
Não darei uma visão completa dos sistemas Pure Type aqui, mas a regra importante (para PTSes funcionais como o CoC) é a seguinte
onde são elementos de um conjunto fixo S das sortes e o par ( s , k ) está em um conjunto fixo R de pares de S , chamados de regras .s,k S (s,k) R S
O insight crucial é que as escolhas cuidadosas de e R fazer grandes diferenças no que o tipo de produto Π x : A . B realmente representa!S R Πx:A.B
Em particular, no cálculo das construções, o conjunto de tipos é { ∗ , ◻ } Freqüentemente chamado Prop e Type (embora essa terminologia seja um pouco confusa para um usuário de Coq por razões de que falarei mais adiante), e a descrição completa conjunto de regras: R = { ( ∗ , ∗ ) , ( ◻ , ◻ ) , ( ◻ , ∗ ) , ( ∗ , ◻ ) }S
E, portanto, temos 4 regras que correspondem a 4 propósitos diferentes:
: Tipos de funções(∗,∗)
Explicarei cada uma delas com mais detalhes.
Com esses tipos e regras extras, você obtém algo que não é um PTS, mas algo próximo. Este é (quase) o Cálculo Estendido de Construções , que está mais próximo da base da Coq. A grande peça que falta aqui são os tipos indutivos, que não discutirei aqui.
Editar: há uma referência bastante interessante que descreve vários recursos das linguagens de programação no âmbito do PTSes, descrevendo um PTS que é um bom candidato para uma representação intermediária de uma linguagem de programação funcional:
Henk: uma linguagem intermediária digitada , SP Jones e E. Meijer.
fonte