5
$\begingroup$

Consider the (big-step) semantics of a language ($a, e$ terms, $v$ values), defined by two mutually recursive relations, $\downarrow$ and $\Downarrow$, given by a set of rule-schemata (simplified):

$\frac{a \cdot x \Downarrow e ~~ e \downarrow v}{a \cdot x \downarrow v}{\tiny PROJECT} ~~~~~~~ \frac{a \downarrow \{ \ldots x = e \ldots \}}{a \cdot x \Downarrow e}{\tiny{FLAT}}$

If I want to prove something about this semantics, I would naturally use induction over rules or judgements. However, when I arrive at rule PROJECT, I would have to make an assertion about $\Downarrow$. And to do so, I would have to return to $\downarrow$.

  1. Is it legit to just merge the proofs for both relations and assume the induction hypothesis for $\Downarrow$ when dealing with $\downarrow$?

  2. Is there some clean way to not merge the proofs but deal with them separately (something similar to break the recursion of functions)?

$\endgroup$
3
$\begingroup$

Yes, it's legit; no, you'll, (usually) have to "merge" the proofs.

You are trying to prove some property of an inductively defined set. You can do so using (structural) induction along the inductive order induced by your definition.

In a nutshell, you'll assume the property for all terms up to "size" (t.b.d.) $n$ (which has to apply to all rule premises) and conclude the property for terms up to size $n+1$ (the conclusions).

In your case, coming up with a good measure of size may be the hardest part, since $a⋅x⇓e$ and $a⋅x↓v$ are of the same "size" if you count operators. What size measure will work is impossible to say without seeing the whole calculus, though. Of course, for structural induction you don't strictly need such a measure; you can just follow the inductive order (see here for examples). As long as your semantics is well-defined, that should work.

$\endgroup$
  • $\begingroup$ Could you elaborate why I need a measure of size? When my relation is defined inductively, that means I have a finite judgement (-tree) at hand. Shouldn't that suffice? I.e. the depth of that tree should define a reasonable size for induction, right? $\endgroup$ – choeger Jul 13 '15 at 18:35
  • $\begingroup$ @choeger Yes, that's a universal measure of size. Be mindful of ambiguities, though. $\endgroup$ – Raphael Jul 13 '15 at 21:08

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.