Em lógica matemática e ciência da computação, o cálculo das construções (CoC) é uma teoria dos tipos criada por Thierry Coquand. Pode servir tanto como uma linguagem de programação tipada quanto como uma fundação construtiva para a matemática. Por esta segunda razão, o CoC e suas variantes têm sido a base para o Rocq e outros assistentes de prova.
Algumas de suas variantes incluem o cálculo das construções indutivas (que adiciona tipos indutivos), o cálculo das construções (co)indutivas (que adiciona coindução) e o cálculo das construções indutivas predicativo (que remove alguma impredicatividade). Características gerais O CoC é um cálculo lambda tipado de ordem superior, inicialmente desenvolvido por Thierry Coquand. É bem conhecido por estar no topo do cubo lambda de Barendregt. É possível dentro do CoC definir funções de termos para termos, termos para tipos, tipos para tipos e de tipos para termos.
O CoC é fortemente normalizante e, portanto, consistente.
Uso O CoC foi desenvolvido juntamente com o assistente de prova Rocq. À medida que funcionalidades eram adicionadas (ou possíveis problemas removidos) à teoria, elas se tornavam disponíveis no Rocq.
Variantes do CoC são usadas em outros assistentes de prova, como Matita e Lean.
O básico do cálculo das construções O cálculo das construções pode ser considerado uma extensão do isomorfismo de Curry–Howard. O isomorfismo de Curry–Howard associa um termo no cálculo lambda simplesmente tipado com cada prova de dedução natural na lógica proposicional intuicionista. O cálculo das construções estende este isomorfismo a provas no cálculo predicativo intuicionista completo, que inclui provas de declarações quantificadas (que também chamaremos de "proposições").
Termos ===
Um termo no cálculo das construções é construído usando as seguintes regras:
é um termo (também chamado de tipo); é um termo (também chamado de prop, o tipo de todas as proposições); Variáveis () são termos; Se e são termos, então também é um termo; Se e são termos e é uma variável, então os seguintes também são termos: , .
Em outras palavras, a sintaxe dos termos, na Forma de Backus-Naur, é então:
O cálculo das construções tem cinco tipos de objetos: provas, que são termos cujos tipos são proposições; proposições, que também são conhecidas como tipos pequenos; predicados, que são funções que retornam proposições; tipos grandes, que são os tipos de predicados ( é um exemplo de tipo grande); o próprio , que é o tipo dos tipos grandes.
β-equivalência === Como no cálculo lambda não tipado, o cálculo das construções usa uma noção básica de equivalência de termos, conhecida como -equivalência. Isso captura o significado da -abstração:
-equivalência é uma relação de congruência para o cálculo das construções, no sentido de que
Se e , então .
Julgamentos === O cálculo das construções permite provar julgamentos de tipagem:
,
que pode ser lido como a implicação
Se as variáveis têm, respectivamente, tipos , então o termo tem tipo .
Os julgamentos válidos para o cálculo das construções são deriváveis de um conjunto de regras de inferência. No que segue, usamos para significar uma sequência de atribuições de tipo ; para significar termos; e para significar ou . Escrevemos para significar o resultado da substituição do termo pela variável livre no termo .
Uma regra de inferência é escrita na forma
,
o que significa
se é um julgamento válido, então também o é.
Regras de inferência para o cálculo das construções === 1.
2.
3.
4.
5.
6.
Definindo operadores lógicos === O cálculo das construções tem muito poucos operadores básicos: o único operador lógico para formar proposições é . No entanto, este único operador é suficiente para definir todos os outros operadores lógicos:
Definindo tipos de dados Os tipos de dados básicos usados na ciência da computação podem ser definidos dentro do cálculo das construções:
Booleanos Naturais Produto União disjunta
Booleanos e Naturais são definidos da mesma forma que na codificação de Church. No entanto, problemas adicionais surgem da extensionalidade proposicional e da irrelevância da prova.
Ver também Sistema de tipos puro Cubo lambda Sistema F Tipo dependente Teoria de tipos intuicionista Teoria de tipos homotópica
Referências
Leitura adicional
Também disponível online gratuitamente: A terminologia é bastante diferente. Por exemplo, () é escrito [x : A] B.
– Uma aplicação do CoC
Categoria:Matemática computacional Categoria:Matemática