# Defining a “repeat until”-construct in Denotational semantics

My Problem is: to define a "repeat until"-construct in terms of Denotational semantics. I made an attempt and now i need to know if i made it right.

The Conditions are: i used the language "While" as specified in "Semantics with Applications" by Nielson & Nielson (1992) (pdf) (WorldCat). I do not want to use the help of the While-construct.

In denotational semantics, we are interested in the effect of a program, rather than in "how" it is executed. Thats why semantic functions are defined compositionally. The corresponding definitions for the Denotational semantics (or "direct style semantics") can be found on page 86 in the Book from Nielson & Nielson (they made it avaible over the Internet).

My Approach is: $$\mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack = \text{FIX }F\\ \text{where }F\ g = \mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack\circ\text{cond}(\mathcal{B}\lbrack\lbrack b\rbrack\rbrack , \mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack\circ g, id)$$

As you might see, my approach is quite similar to the definition of while, but i cannot see a mistake in it.

post scriptum: Bounty given, and second edit: yes, i meant $$\mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack$$ .. typo corrected.

• $f \circ g$ means do $g$ first and $f$ afterwards. You seem to think of it backwards. Secondly, the repeat-until loop stops when $b$ becomes true. You are making it continue when $b$ is true and stop if $b$ is false. – Uday Reddy Nov 21 '13 at 16:00

Presumably you mean $\lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack$, which you can easily define using $\text{while}$ as follows.

$$\mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack = \mathcal{S}_{\text{ds}} \lbrack\lbrack S ; \text{while } \lnot b \text{ do } S\rbrack\rbrack$$

Note that typically, a $\text{repeat}$ construct loops while the condition is false; your definition keeps the condition positive.

Building on the above equation and expanding the right-hand side using the table on page 86, you get:

$$\mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack = (\text{FIX }F)\circ \mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack\\ \text{where }F\ g = \text{cond}(\mathcal{B}\lbrack\lbrack \lnot b\rbrack\rbrack , g\circ\mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack, id)$$

You can transform the above to the following.

$$\mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack = \text{FIX }F\\ \text{where }F\ g = \text{cond}(\mathcal{B}\lbrack\lbrack \lnot b\rbrack\rbrack, g, id)\circ \mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack$$

Your version is not correct in this regard, it would be equivalent to $\lbrack\lbrack \text{while } b \text{ do } S;S\rbrack\rbrack$, which evaluates the condition before rather than after the first execution of $S$.

• thanks for the answer, please give me a day to think about it – Toralf Westström Nov 18 '13 at 19:23
• next question: don't you think there is still an error in your Definition? i don't get the sense of the $\mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack$ within the -cond-Statement. Wouldn't be it correct to write: $$\mathcal{S}_{\text{ds}} \lbrack\lbrack\text{repeat } S \text{ until } b\rbrack\rbrack = \text{FIX }F\\ \text{where }F\ g = \text{cond}(\mathcal{B}\lbrack\lbrack \lnot b\rbrack\rbrack , g, id)\circ \mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack$$ Otherwise you would perform the S-Statement twice for each Loop, or not? – Toralf Westström Nov 21 '13 at 15:02
• @ToralfWestström, yes, I actually made a few mistakes, give me a little time to edit. In particular, pushing $\mathcal{S}_{\text{ds}} \lbrack\lbrack S\rbrack\rbrack$ into $F$ is incorrect as you correctly note, the statements would be performed twice. The version you mention in the comment seems correct at the first glance. – avakar Nov 22 '13 at 20:25
• Also, I have $\mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack\circ g$ in the $\text{cond}$ statement inverted, it should be $g\circ\mathcal{S}_{\text{ds}}\lbrack\lbrack S\rbrack\rbrack$. – avakar Nov 22 '13 at 20:34