4
$\begingroup$

I want to express a simple correctness theorem for a term-desugaring function $\Delta$. The goal is to express that if the evaluation of a desugared term yields a value, this value is the desugared result of evaluating the original term.

Since the implication operator $\Rightarrow$ is already used in my dynamic semantics, I'd rather use an inference rule to express the implication. However, in the premise I have to introduce a variable $v$ that is the result of applying $\Delta$ to a variable bound in the conclusion. Since there is no inverse of $\Delta$ I am somewhat stuck between two odd variants to express the relation.

The first variant uses two conclusions (like multiple premises the idea is that both always hold):

$$ \frac{\Delta(t) \Downarrow v}{t \Downarrow v^\prime \quad \Delta(v^\prime) = v} $$

This looks odd to me. The alternative would be to see the rule as a scheme subject to some substitution over the meta-variables $t$ and $v$. In that case I could also write:

$$ \frac{\Delta(t) \Downarrow \Delta(v)}{t \Downarrow v} $$

This is obviously cleaner, but I am not quite happy with the implications (pun not intended) to the theorem: In the first case, if $v \neq \Delta(v^\prime)$ the premise still holds, but the conclusion does not, so $\Delta$ is not correct. In the second case the premise would not apply - so correctness simply does not cover the case at all.

Is there a common pattern to deal with such problems? Did I overlook something?

$\endgroup$
  • 1
    $\begingroup$ Could you state in English the proposition that you want to express? With the first rule, you seem to be trying to say “if $\Delta(t) \Downarrow v$ then there exists $v'$ such that $\Delta(v') = v$ and $t \Downarrow v'$”. With the second rule, you seem to be trying to say that if $\Delta(t) \Downarrow \Delta(v')$ then $t \Downarrow v'$ (with no implication if $v'$ isn't a desugaring). Is the problem with the first rule the existence of $v'$ or its choice? $\endgroup$ – Gilles 'SO- stop being evil' Oct 6 '15 at 12:14
  • $\begingroup$ I want to express the theorem that if a desugared term evaluates to a value this value is the result of applying desugaring to the result of evaluating the non-desugared term (which has to exist). So your interpretation of the first rule is exactly my intention. However, I find it odd to have multiple statements in the conclusion, especially if one of these statements is non-inductive. $\endgroup$ – choeger Oct 6 '15 at 14:00
3
$\begingroup$

Let us introduce an auxiliary predicate $t \downarrow$ whose intended meaning is "$t$ evaluates to something". Its inference rule is $$\frac{t \Downarrow v}{t \downarrow}.$$ Now you can express your condition with the following two rules:

  1. If $\Delta(t)$ evaluates to $v$ and $t$ evaluates $v'$ then $v$ equals $\Delta(v')$: $$\frac{\Delta(t) \Downarrow v \qquad t \Downarrow v'}{\Delta(v') = v}$$

  2. If $\Delta(t)$ evaluates to something then so does $t$: $$\frac{\Delta(t) \downarrow}{t \downarrow}$$.

This is not quite the same as using first-order logic and writing $(\exists v . \Delta(t) \Downarrow v) \implies \exists v' . t \Downarrow v'$. You have to go "meta" and use inversion to conclude from $t \downarrow$ that there exists $v'$ such that $t \Downarrow v'$.

By the way, you said that "since the implication operator $\Rightarrow$ is already used in my dynamic semantics, I'd rather use an inference rule to express the implication" That's a pretty awful reason to choose inference rules over axioms (which is what an implication would give you). You should ask instead what your semantics is for. If you are interested in operational semantics, i.e., you want to express how your programs will be executed, then the rule you are talking about does not really contribute anything. If you want your semantics for reasoning about $\Delta$ and $\Downarrow$, then it might actually be use good old first-order logic.

$\endgroup$
  • $\begingroup$ Could you elaborate a bit on the "awful reason"? AFAIK, an inference rule is an implication (implicitly all-quantified over the meta variables in the premises) and the "link" to an inductive relation is more a convention. In other words, my theorem would be an admissable rule (I think that is the correct terminus) of the evaluation/desugaring system. $\endgroup$ – choeger Oct 15 '15 at 17:33

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.