Assume a language with statements such as $x := e$, $\text{assume}(e)$, etc., and particularly a $\text{split}\ stmt_1 ... stmt_n$ statement, constructed from $n$ statements. Informally, the semantics of this statement is that each statement is evaluated separately, and if exactly one such evaluation terminates (i.e. is not stuck) then the result of the split statement (expressed as the new state) is the result of that evaluation. I'm trying to express this semantic formally using a big-step evaluation rule. Here is my try:

$$ \dfrac {stmt_i\ |\ \mu \Downarrow \mu_i' \wedge \forall j \neq i. (\not\exists \mu_j'.\ stmt_j\ |\ \mu\ \Downarrow \mu_j')} {\textbf{split}\ stmt_1 ... stmt_n\ |\ \mu \Downarrow \mu_i'}\text{E-Split-i} $$


The statement "$\textbf{split}\ stmt_1 ... stmt_n$" evaluated in context $\mu$ results in context $\mu_i'$ if its $i$th statement evaluated in context $\mu$ results in context $\mu_i'$ and there is no other statement among $\{stmt_1, ..., stmt_{i-1}, stmt_{i+1}, ..., stmt_n\}$ for which there exists a context $\mu_j'$ such that evaluating this statement in context $\mu$ results in context $\mu_j'$. (Implying that the evaluation of every other statement is stuck at some point.)

Is my rule correctly formalized? Is there a better way of writing it?

  • $\begingroup$ It looks OK. Maybe use two premises instead of $\land$. However, I am a bit scared by this exercise. First, it uses negation in a premise, which prevents one to invoke Tarski's fixed point theorem and claim that the relation is well-defined. In general, a least fixed point does not exist with negative premises, and one has to prove it explicitly case-by-case (e.g. using stratification). Second, if the language is Turing-powerful, the negative premise checks for non-termination, which is a non-RE property. This is not a problem of your solution, but of the question. $\endgroup$ – chi Feb 4 '18 at 17:04
  • $\begingroup$ @chi Thank you for expressing your concerns, it is particularly helpful considering the fact that this is not my solution to an exercise but something I am doing on my own. Moreover, I think you might be right that there is something inherently wrong with split because it would require checking for non-termination of the other statement and the language is indeed turing-powerful. I guess I could make it weaker by requiring the evaluation to be stuck within $k$ small-steps. $\endgroup$ – Romain Beguet Feb 4 '18 at 17:45

Your Answer

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

Browse other questions tagged or ask your own question.