Inference rule with two conclusions or rather inverse function application

Question

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?

Answer 1

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.