Klasa funkcji obliczalna przez Coq

Ponieważ nie pozwala na niekończące się obliczenia, Coq niekoniecznie nie jest kompletny w Turingu. Jaką klasę funkcji może obliczyć Coq? (czy istnieje ich interesująca charakterystyka?)

computability pl.programming-languages coq

— Steve
źródło

Benjamin Werner udowodnił wzajemną interpretację ZFC z niezliczoną liczbą niedostępnych i rachunku konstrukcji indukcyjnych w swoim artykule Zestawy w typach, Typy w zestawach .

Oznacza to z grubsza, że dowolna funkcja, która może być pokazana jako całkowita w ZFC z niezliczoną liczbą niedostępnych, może być zdefiniowana w Coq. Więc jeśli nie jesteś teoretykiem zestawów pracującym na dużych kardynałach, jest mało prawdopodobne, aby jakakolwiek funkcja obliczeniowa, jakiej kiedykolwiek chciałeś, nie mogła zostać zdefiniowana w Coq.

— Neel Krishnaswami
źródło

Z wyjątkiem tłumacza Coq ...

— Jules

W rzeczywistości można zaimplementować interpreter języka Coq (a właściwie dowolne ogólne funkcje rekurencyjne) w Coq. Jeśli CIC jest spójny, nie będziesz w stanie udowodnić, że interpreter jest funkcją całkowitą, oczywiście, ale na pewno możesz ją zaimplementować.

— Neel Krishnaswami,

Możesz użyć konstruktywnej monady windowej, , aby napisać ogólne funkcje rekurencyjne. Wówczas Twój typechecker będzie miał typ

. Jest to w zasadzie podejście Bove / Capretta. (Zobacz także Bentona, Kennedy'ego i Varminga „Some Domain Theory and Denotational Semantics in 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: To oszustwo. I nie bez powodu, mielibyśmy niespójność.

— Andrej Bauer,

To oszustwo, ponieważ funkcja oceny ma oceniać rzeczy, a nie dawać ci brak odpowiedzi.

— Andrej Bauer,