The Stack Overflow podcast is back! Listen to an interview with our new CEO.

Questions tagged [denotational-semantics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
0answers
21 views

What is the difference between programming and planning? Is programming the special case of planning?

Computer programming is laying out the predefined operations (actions) in compositional/recursive/recurrent manner to go from one defined state (e.g. assignment of variables) to the other defined ...
4
votes
1answer
584 views

What's the difference between: operational, denotational and axiomatic semantics?

Recap of the terms from the dictionary: semantics: the study of meaning in a language (words, phrases, etc) and of language constructs in programming languages (basically any syntactically valid part ...
3
votes
2answers
75 views

Why does the denotational semantics for a while loop have a existence quantifier?

I was going through these notes and they have the following operator on partial functions: $$ \mathcal F^{k}(\bot)(\sigma) = \left\{ \begin{array}{ll} \alpha( [\![s]\!]\sigma ) & [\![b]\!]\...
1
vote
2answers
71 views

How is it that programs can be identified with partial functions for programming language semantics?

I was reading about denotational semantics Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, ...
3
votes
0answers
58 views

What Happened to “Top” in Denotational Semantics?

Has "top" ($\top$) been removed from or relegated to a much more minor role in denotational semantics? If so, when and why? I see older papers and books talking about both "top" and "bottom" ("bot", $...
12
votes
4answers
2k views

What does the leading turnstile operator mean?

I know that different authors use different notation to represent programming language semantics. As a matter of fact Guy Steele addresses this problem in an interesting video. I'd like to know if ...
5
votes
1answer
108 views

Domain theory: Definition of isomorphisms

Consider the following definitions of CPOs, monotonicity and continuity: The pair $(M, \leq)$ is called CPO (complete partial order), if $M$ is a set, $\leq$ is a partial order on $M$, there exists a ...
7
votes
1answer
681 views

Why are computable functions continuous?

I am working on writing an easy to read document about denotational semantics of the lambda calculus. For that I introduce CPOs, monotonicity and continuity. A CPO is a set $M$ with a partial order $\...
3
votes
0answers
438 views

How to decide between operational, denotational, and axiomatic semantics?

Context I'm designing a language which implements lambda calculus and (first-order) predicate calculus, where lambdas behave as the abstraction encapsulating logic, compositionally forming a ...
7
votes
1answer
212 views

What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

I'm reading through a commentary on Milner's "The use of machines to assist in rigorous proof" by Mike Gordon. In this paper, he explains how LCF was born from the ideas of denotational semantics by ...
6
votes
0answers
151 views

Is there relation between K-Framework and structural operational semantics?

K-framework strives to give one (instead of two - operational and denotational) semantics for industrial programming languages. The same unification is done by structural operational semantic as well. ...
14
votes
2answers
368 views

What questions can denotational semantics answer that operational semantics can't?

I am familiar with operational semantics (both small-step and big-step) for defining programming languages. I'm interested in learning denotational semantics as well, but I'm not sure if it will be ...
3
votes
0answers
105 views

What is the semantic model of types?

By reading literature on (denotational) semantics of types, I see that people tried to give several models of types. Reynolds showed that types in general cannot be given a set semantics in classical ...
3
votes
1answer
816 views

What is a predicate transformer?

I'm reading Programming - The derivation of algorithms, and I want to understand the purpose of a predicate transformer. This is the excerpt (p. 14-15): A more precise way in which constructs may ...
9
votes
0answers
116 views

Denotational semantics of object-oriented languages

I am interested in denotational semantics of object oriented languages. Namely, what are the common/typical denotations of objects used in the literature? Is this an interesting topic these days? The ...
2
votes
0answers
38 views

Where, besides Scheme reports (RnRS) has Stoy's notation for auxiliary semantic functions been used?

The denotational semantics of R4RS, R5RS and R7RS Scheme (included in the language report) uses the same notation that was used by J. E. Stoy in his book, "Denotational Semantics: the Scott-Strachey ...
2
votes
1answer
49 views

Prove an arithmetic property of a partial recursive function

I have this program written in haskell : I have to prove that: $(\forall a \in \mathbb{N})[!D_V [h](a) \Rightarrow log_2 (D_V[h](a) )\equiv 2 (mod$ $ 10) ]$. The predicate $P_2$ for the $g$ ...
3
votes
0answers
119 views

Scott/Lawson topology for function space domain

Given two domains, $D_1$, $D_2$, already equipped with Scott (or Lawson) topology, the product domain $D=D_1\times D_2$ has the Tychonoff product topology, e.g., Mathematical Theory of Domains, ...
1
vote
1answer
48 views

denotional semantic for while - fixed points

In my book it is written: $$[[\text{while b do S}]] = \text{FIX F}$$, where $Fg = cond (\beta[[b]], g\circ [[S]], id). $ What is cond ? $[[\text{if b then S1 else S2}]] = cond (\beta[[b]], [[S1]], [[...
4
votes
1answer
530 views

Denotational semantics of expressions with side effects

I'm doing revision for a module on programming language semantics and I'm having trouble understanding the introduction of side-effects in expressions. We assume a standard syntax for arithmetic ...
1
vote
1answer
78 views

Defining function for arithmetic expressions

I've got these arithmetic expressions a ::= n | x | a1 + a2 | a1 ? a2 | a1 − a2 which are a part of language. An undefined element is allowed ⊥ ...
5
votes
1answer
1k views

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 ...
2
votes
0answers
355 views

Example of execution fragment of multi-process transition system

Here is a simple transition system of beverage vending machine: The exemplary execution fragments can look like this: Now, imagine we have multi-process TS where processes are identical and ...
3
votes
2answers
954 views

how do you define functions with denotational semantics?

Denotational semantics are abstract functions that give meaning to statements of a programming language. They accept an expression and return a value. But how do you define denotational semantics for ...
2
votes
1answer
122 views

Homomorphisms and isomorphisms in an equational calculus

Suppose we have an algebraic specification in the form: $\{S,F,w\}$ where $S$ are the sorts, $F$ are the functions and $w$ are the set of equations. For example, the specification for natural numbers: ...