Dado um termo t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))
na teoria de tipos de Martin-Lof, qual é o valor de w(t(0))
, onde w
está o operador que extrai a testemunha de um termo de tipo existencial?
12
Dado um termo t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))
na teoria de tipos de Martin-Lof, qual é o valor de w(t(0))
, onde w
está o operador que extrai a testemunha de um termo de tipo existencial?
Respostas:
fonte
Para demonstrar a resposta de Mark, considere a seguinte prova
t
de sua declaração, escrita em Coq. Na prova, assumimos que um parâmetrok
do tiponat
é fornecido. Usamosk
como valor dey
casox = 0
:Podemos provar que
t 0
é igual ak
:O
protT1
está lá porquet 0
não é apenas um número natural, mas na verdade um número natural com uma prova de que0 <> 0 -> 0 = S y
eprojT1
joga fora a prova.O código Ocaml extraído para
t
, obtido com o comandoExtraction k
éNovamente, podemos ver que
t 0
é igual ak
, que era um parâmetro assumido arbitrariamente.fonte