Question

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.

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top