[Solved]: Defining a "repeat until"-construct in Denotational semantics

Problem Detail: 

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.

Asked By : Toralf Westström

Answered By : avakar

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$.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/18054