Classe de funções computáveis pela Coq

Benjamin Werner provou a interpretabilidade mútua do ZFC com muitos inacessíveis e o Cálculo de Construções Indutivas, em seu artigo Sets in Types, Types in Sets .

Isso significa, grosso modo, que qualquer função que possa ser mostrada como total no ZFC, com muitos inacessíveis, pode ser definida no Coq. Portanto, a menos que você seja um teórico dos conjuntos trabalhando em cardeais grandes, é improvável que qualquer função computável que você já desejou não possa ser definida no Coq.

Neel Krishnaswami
fonte

Exceto um intérprete Coq ...

Jules

Na verdade, você pode implementar um intérprete Coq (de fato, funções recursivas gerais arbitrárias) dentro do Coq. Se o CIC for consistente, você não poderá provar que o intérprete é uma função total, é claro, mas você pode definitivamente implementá-lo.

Neel Krishnaswami

Você pode usar a mônada de elevação construtiva,

, para escrever funções recursivas gerais. Em seguida, o seu typechecker terá tipo

. Essa é basicamente a abordagem Bove / Capretta. (Veja também Benton, Kennedy e Varming de "algum domínio Teoria e denotacional Semântica em Coq",dl.acm.org/citation.cfm?id=1616077.1616090.)

A_{⊥} ≜ ν α . A + α

$A_\bot \triangleq \nu \alpha.\; A + \alpha$

c o n t e x t \to t e r m \to t y p e \to {b o o l}_{⊥}

$\mathsf{context} \to \mathsf{term} \to \mathsf{type} \to \mathsf{bool}_\bot$

Neel Krishnaswami

@ Neel: Isso é trapaça. E por uma boa razão, caso contrário, teríamos uma inconsistência.

Andrej Bauer

É trapaça porque a função de avaliação deve avaliar as coisas, não fornecer uma não resposta.

Andrej Bauer 22/01

Classe de funções computáveis ​​pela Coq

Respostas:

Classe de funções computáveis pela Coq