12
$\begingroup$

Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where w is the operator that extracts the witness of a term of existential type?

$\endgroup$
  • $\begingroup$ I think you mean $\neg(x=0)$. $\endgroup$ – Mark Reitblatt Nov 29 '10 at 21:41
  • $\begingroup$ Yes, Mark, thanks for pointing out that, fixed. $\endgroup$ – day Nov 29 '10 at 22:16
12
$\begingroup$

Any value. It depends upon which $t$ you are given. A term of type $\exists y.(\neg(0 = 0) \Rightarrow 0 = S(y))$ is a pair of an int $y$ and a function that takes a proof of $\neg(0=0)$ and gives you a proof of $0 = S(y)$. You can use a term of type $\neg(0 = 0)$ and type $0 = 0$ (from reflexivity) to derive a term of any type you want. This includes a term of type $0 = S(0)$, $0 = S(1)$, $\ldots$. So, you can make $y$ any integer you want.

$\endgroup$
10
$\begingroup$

To demonstrate Mark's answer, consider the following proof t of your statement, written in Coq. In the proof we assume that a parameter k of type nat is given. We use k as the value of y in case x = 0:

Parameter k : nat.

Theorem t : forall x : nat, { y : nat | x <> 0 -> x = S y}.
Proof.
  induction x.
  exists k; tauto.
  induction x.
  exists 0; auto.
  destruct IHx as [z G].
  exists (S z).
  intro H.
  elim G; auto.
Defined.

We can prove that t 0 is equal to k:

Theorem A: projT1 (t 0) = k.
Proof.
  auto.
Qed.

The protT1 is there because t 0 is not just a natural number, but actually a natural number with a proof that 0 <> 0 -> 0 = S y and projT1 throws away the proof.

The extracted Ocaml code for t, obtained with the command Extraction k is

(** val t : nat -> nat **)

let rec t = function
  | O -> k
  | S n0 -> (match n0 with
              | O -> O
              | S n1 -> S (t n0))

Again we can see t 0 is equal to k, which was an aribtrarily assumed parameter.

$\endgroup$
  • $\begingroup$ Thanks for the example in Coq, Andrej, it clarifies more. $\endgroup$ – day Dec 17 '10 at 16:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.