Вопрос

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.

Нет правильного решения

Лицензировано под: CC-BY-SA с атрибуция
Не связан с cs.stackexchange
scroll top