Dado un término t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))
en la teoría de tipos de Martin-Lof, ¿cuál es el valor de w(t(0))
, dónde w
está el operador que extrae el testigo de un término de tipo existencial?
12
Dado un término t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))
en la teoría de tipos de Martin-Lof, ¿cuál es el valor de w(t(0))
, dónde w
está el operador que extrae el testigo de un término de tipo existencial?
Respuestas:
fuente
Para demostrar la respuesta de Mark, considere la siguiente prueba
t
de su declaración, escrita en Coq. En la prueba asumimos que se da un parámetrok
de tiponat
. Usamosk
como el valor dey
en casox = 0
:Podemos demostrar que
t 0
es igual ak
:El
protT1
está ahí porquet 0
no es sólo un número natural, pero en realidad un número natural con una prueba de que0 <> 0 -> 0 = S y
yprojT1
desecha la prueba.El código Ocaml extraído para
t
, obtenido con el comandoExtraction k
esDe nuevo, podemos ver que
t 0
es igual ak
, que era un parámetro asumido de forma arbitraria.fuente