3
$\begingroup$

In Harper's Practical Foundations for Programming Languages, page 19, rule (2.9) defines the $sum$ function inductively.

$$ \frac{b:nat}{sum(zero;b;b)}\tag{rule 2.9a} $$

$$ \frac{sum(a;b;c)}{sum(succ(a);b;succ(c))}\tag{rule 2.9b} $$

Then the author introduced Theorem 2.4 to prove $sum$ is indeed a function, that is, $c:nat$ is guaranteed to exist and to be unique for any $a:nat$ and $b:nat$.

The proof of existence does a rule induction on $a:nat$. This is essentially a mathematical induction on a single variable. I think I understand the proof and can translate it into a formal one without much difficulty.

But the proof of uniqueness frustrates me a lot.

First, the author decides to do the induction on rule 2.9 (rather than 2.2). My understanding is that here we can have a set-theoretic view of the function $sum$. It could be thought of as a relation $\Sigma$, a subset of $\mathbb{N}\times\mathbb{N}\times\mathbb{N}$. Each element $r \in \Sigma$ is a 3-tuple $\langle a,b,c\rangle$ where $a,b,c \in \mathbb{N}$. The set $\Sigma$ is inductively defined by rule 2.9. From this viewpoint, a structural induction on $\Sigma$ is perfectly acceptable (as a newbie I spent substantial amount of time to figure this out).

The author states the property to be held as "if $sum(a;b;c_1)$, then if $sum(a;b;c_2)$, then $c_1\;is\;c_2$", which could be straightforwardly translated into

$$ sum(a;b;c_1) \rightarrow (sum(a;b;c_2) \rightarrow c_1\;is\;c_2)\tag{a} $$

But I am not sure whether it is a single variable predicate $\mathcal{P}(sum(a;b;c_1))$, or a two-variable one $\mathcal{P}(sum(a;b;c_1),sum(a;b;c_2))$. Since "an inner induction" is mentioned in both parts (2.9a and 2.9b), it seems the latter is in author's mind, but I have no idea how a two-variable induction works.

In the induction step (rule 2.9b) the author seems to put the induction hypothesis as

$$ sum(a^\prime;b;c_1^\prime) \rightarrow (sum(a^\prime;b;c_2^\prime) \rightarrow c_1^\prime\;is\;c_2^\prime)\tag{b} $$

then the goal is to prove something like

$$ sum(a;b;c_1) \rightarrow (sum(a;b;c_2) \rightarrow c_1\;is\;c_2)\tag{c} $$

where $a,c_1,c_2$ are successors of their primed version respectively.

I understood the statement "We have that $a\;is\;succ(a^\prime)$ and $c_1\;is\;succ(c_1^\prime)$, where $sum(a^\prime;b;c_1^\prime)$." as

$$ sum(a^\prime;b;c_1^\prime) \rightarrow sum(a;b;c_1) \tag{d} $$

and "we may show that if $sum(a;b;c_2)$, then $c_2\;is\;succ(c_2^\prime)$ where $sum(a^\prime;b;c_2^\prime)$" as

$$ sum(a^\prime;b;c_2^\prime) \rightarrow sum(a;b;c_2) \tag{e} $$

Even each piece looks reasonable, I failed to combine those pieces into a whole picture. I expect from induction hypothesis (b), with rules 2.9, natural deduction rules of first order logic, $\mathcal{P}(conclusion)$ (c) should be arrived. But I cannot figure out how. I get stuck here.

The author's proof is intuitively correct. But I do hope to see:

  1. a formal proof, or an explanation or clarification from where a formal proof can easily be constructed.
  2. confirmations or corrections of the descriptions and predicates above.
  3. if this is a two-variable induction, how it works (in the context of rule induction)?
$\endgroup$
2
  • $\begingroup$ Can you please add the definition of the sum function and the rule in the question text. It would make the question more comprehensive. $\endgroup$
    – Apoorv
    Commented Feb 24, 2023 at 18:58
  • $\begingroup$ @Apoorv rule 2.9 added. :) $\endgroup$ Commented Feb 24, 2023 at 19:49

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.