Étant donné un terme t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))
dans la théorie des types de Martin-Lof, quelle est la valeur de w(t(0))
, où w
est l'opérateur qui extrait le témoin d'un terme de type existentiel?
lo.logic
type-theory
proof-theory
journée
la source
la source
Réponses:
la source
Pour démontrer la réponse de Mark, considérez la preuve suivante
t
de votre déclaration, écrite en Coq. Dans la preuve, nous supposons qu'un paramètrek
de typenat
est donné. Nous utilisonsk
la valeur dey
dans le cas oùx = 0
:Nous pouvons prouver que
t 0
c'est égal àk
:Le
protT1
est là parcet 0
est non seulement un nombre naturel, mais en fait un nombre naturel avec une preuve0 <> 0 -> 0 = S y
etprojT1
jette la preuve.Le code Ocaml extrait pour
t
, obtenu avec la commandeExtraction k
estEncore une fois, nous pouvons voir que
t 0
est égal àk
, qui était un paramètre présumé aribtrairement.la source