Questions tagged [denotational-semantics]
The denotational-semantics tag has no usage guidance.
49 questions
3
votes
2
answers
226
views
The meaning of the recursive type μt.t
In the paper:
David B. MacQueen, Gordon D. Plotkin, Ravi Sethi: An Ideal Model for Recursive Polymorphic Types. Inf. Control. 71(1/2): 95-130 (1986).
the authors give a domain theoretic model for a ...
- 367
0
votes
1
answer
223
views
What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?
In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of ...
- 599
3
votes
1
answer
147
views
Is there a full abstraction result for an untyped lambda calculus?
Famously, the denotational semantics of PCF in Scott domains is not fully abstract. But by adding the parallel or construct to PCF, a fully abstract semantics can be obtained.
Is there an analogous ...
- 225
4
votes
2
answers
266
views
Denotational semantics of intersection types
Is there a denotational (possibly, domain theoretic) semantics of intersection types? If yes, could you provide some references?
Let me try to give some context to my question. In the usual ...
- 367
11
votes
2
answers
405
views
What are pertinent references to cite on Scott domains?
Scott domains are often presented as having been introduced in 1969. However, the first (but numerous!) papers are from the 1970s, so it is not easy to know what the pertinent references are. My two ...
- 509
4
votes
2
answers
279
views
Operational semantics and denotational semantics and describing the behaviour and structure of programs
I was under the impression that operational semantics describes the behaviour of a program (so it includes the implementation details / the implementation matters), whereas denotational semantics ...
- 171
1
vote
0
answers
57
views
Is this proof for completeness of regular model checking correct?
In "Calculational Design of A Regular Model Checker by Abstract Interpretation" by Patrick Cousot (link), on page 15 it can be seen that to prove the completeness of regular model checking (...
- 13
7
votes
1
answer
594
views
The precise definition of Normalization By Evaluation?
The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language:
The ...
- 105
10
votes
1
answer
186
views
What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?
I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the ...
- 387
12
votes
2
answers
616
views
Induction-recursion in models other than $\mathbf{Set}$
It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
- 333
4
votes
1
answer
141
views
A possible error in the semantic chapter of the ISO standard for the Z specification notation
I may have found an error in the ISO standards document for the Z specification notation, namely ISO/IEC 13568:2002, "Information technology — Z formal specification notation — Syntax, type ...
- 364
6
votes
0
answers
123
views
Is there a known notion of "stochastic dependent pair"?
I came upon this when thinking about the semantics of probabilistic programs. Say you have a generative model
N ~ Poisson()
for n = 1:N
X[i] ~ Normal()
Then the ...
- 229
6
votes
1
answer
153
views
Given a domain, how do we build a language whose denotation is the domain?
Say we have an arbitrary domain $D$ with a countable basis $B$. Now, how do i build a "language" whose "denotation" lives in the domain?
My understanding is that Dana Scott ...
- 605
9
votes
0
answers
206
views
Results in denotational semantics from model theory?
Denotational semantics interpret the theories of various lambda calculi in various (set-theoretic, domain-theoretic, category-theoretic, game...) models. Let $T$ be the theory of one such lambda ...
- 1,195
10
votes
0
answers
450
views
Typed Lambda Calculus models and denotations
I'm trying to draw a general mental picture about the models and the
denotational semantics of the typed lambda calculus, in its different
variants.
I'm particularly interested in how the semantics ...
- 688
8
votes
0
answers
384
views
Denotational semantics of System $F_\omega$ with recursive types and general recursion
Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion?
I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
- 161
1
vote
1
answer
155
views
Observational Equivalence of open terms in PCF
The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms.
Lets consider the simple case where the terms ...
- 31
8
votes
2
answers
511
views
Precise definition of syntatic categories / syntatic domains in abstract syntax
I have read the introductory parts of a couple of books on programming language semantics (Gordon, Winskel, Nielson & Nielson, Allison, Stump, Schmidt), and while I do understand what they mean by ...
- 235
1
vote
0
answers
86
views
Categorical way of factoring out points
Major rewrite justifiably asked for:
I'm currently trying to get a categorical way of doing something called the Gelfond-Lifschitz reduct on a set of single-headed Horn clauses. The semantics is the ...
- 191
3
votes
1
answer
176
views
What is contextual equivalence ignoring non-termination called?
Contextual equivalence ($M_1 \cong_{ctx} M_2$) is often defined as:
$C[M_1] \Downarrow V \iff C[M_2] \Downarrow V$
Which is to say for any context $C$, $C[M_1]$ terminates with value $V$ iff $C[M_2]$...
- 133
1
vote
1
answer
1k
views
What is the relation/difference between axiomatic and denotational semantics one one side, and the data flow analysis(DFA) on the other sied?
I am supposed to write a small paper about DFA in OOP for a CS class in theory. But I am required to connect that (DFA) to axiomatic and denotational semantics!
I read few resources about axiomatic/...
- 113
7
votes
1
answer
146
views
In which posets is the set of compact elements downwards closed?
In a poset $(D, \sqsubseteq)$, a compact element is an element $d \in D$ such that for every directed set $A$ which happens to have a supremum $\bigsqcup A \in D$ with $d \sqsubseteq \bigsqcup A$, it ...
- 371
5
votes
1
answer
189
views
What are Zhang's molecules?
I'm currently looking into the representation theory of Scott domains. In his paper "dI-Domains as prime information systems" (1992), Guo-Qiang Zhang uses prime information systems to represent dI-...
- 371
10
votes
3
answers
599
views
Is there any known CCC closed under a probabilistic powerdomain operation?
Equivalently, is there a known denotational semantics for probabilistic higher-order functional programming languages? Specifically, is there a domain model of pure untyped $\lambda$-calculus extended ...
- 265
5
votes
2
answers
1k
views
Flat vs non-flat domains
My understanding is that, more often than not, when people use domain theory for higher-type computability or the denotational semantics of functional programming languages, they tend to prefer flat ...
- 371
1
vote
1
answer
175
views
Name a set of program variables
I am interested in the set of the variables that satisfy the following properties. I would like to find a proper name for them.
We assume that a program $\phi$ has a set of variables $v_0, \ldots, ...
- 73
8
votes
2
answers
464
views
Categorical semantics for non-monotonic logics?
Are there any categorical semantics for non-monotonic logics?
It appears that the simple answer to this is "No" since the obvious notion of composition fails for any model of a non-monotonic logic. ...
- 191
3
votes
2
answers
298
views
What requirements should a denotational semantics for a programming language satisfy to be correct?
We have a programming language and its denotational semantic,
like Tony Hoare's CSP with its syntax and denotational semantic
e.g. stable failure and UTP.
We want to extend the language (its ...
- 31
8
votes
0
answers
188
views
Equivalence of categories of directed complete posets
I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets.
Since I had no answer, I try here.
In the book ``Domains and Lambda-...
- 181
18
votes
2
answers
2k
views
Full Completeness vs Full Abstraction of a program translation
Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences.
Instead of providing full abstraction proofs, some ...
- 485
7
votes
0
answers
269
views
Types as theories
I am studying Goguen's paper Types as theories [1].
Based on Goguen's paper, are the following true?
Subsort inheritance provides a classification of values, every value of the sub-sort is a value of ...
- 179
0
votes
2
answers
288
views
Meaning of program as solution of a recursive equation
I would like to ask you a question about (denotational?) semantic of program. After defining program as a transition system, and the semantics as a transition function: $$next: States \rightarrow ...
- 732
0
votes
0
answers
92
views
Semantics of a programming language [duplicate]
A newbie question, if I may... Could you be so kind and explain to me in plain english meaning of 'denotational semantics' and 'operational semantics'? I'm familiar with the definitions and have read ...
- 101
13
votes
1
answer
2k
views
Can Scheme's call/cc implement all known control flow structures?
The page "Advanced Scheme: Some Naughty Bits" states:
Continuations are a powerful control-flow construct from which
nearly any other control-flow structure [...] may be derived.
I thought that ...
- 133
10
votes
1
answer
2k
views
What is the difference between meaning and denotation?
In programming language semantics, it is often heard that people talking about meaning and denotation. They seem not to be the same. What is the difference? Is the former associated with ...
- 2,845
19
votes
2
answers
1k
views
A mathematical (categorical) description of type classes
A functional language can be viewed as a category where its objects are types and morphisms functions between them.
How do type classes fit in this model?
I assume we should only consider those ...
- 2,611
16
votes
2
answers
508
views
Uses of quasi-PERs/difunctional relations/zig-zag relations?
Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property:
If $a \sim b$ and $a' \sim b'$ and $a \sim ...
- 32.9k
10
votes
1
answer
198
views
Reference for the undefinability of modulus of continuity functional in PCF?
Can someone point me to the reference for the non-definability of the modulus of continuity functional in PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$
Andrej Bauer has ...
- 32.9k
10
votes
1
answer
430
views
Reasoning about non-deterministically terminating loops
Here's a "track B" question if there ever was one. Summary: the first thing I think of when I try to give a semantics to non-deterministic programs results in a semantics where I can't prove things ...
- 2,396
17
votes
2
answers
1k
views
What is the origin of logical relations?
I actually have two questions:
Who first used logical relations to relate semantics?
I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim to ...
- 2,717
7
votes
1
answer
261
views
Has anyone studied "polynomially compact" metric spaces?
A subspace $S$ of a metric space $A$ is compact if it is complete and totally bounded. Here, complete means that every Cauchy sequence in $S$ has a limit also in $S$. For $S$ to be totally bounded, ...
- 32.9k
15
votes
1
answer
648
views
Fixed point theorems for constructive metric spaces?
Banach's fixed point theorem says that if we have a nonempty complete metric space $A$, then any uniformly contractive function $f : A \to A$ it has a unique fixed point $\mu(f)$. However, the proof ...
- 32.9k
11
votes
1
answer
353
views
Is Escardó's metric semantic for PCF+timeouts fully abstract ?
In his 1999 workshop paper "A Metric Model of PCF", Martín Escardó showed that it is possible to give a simple interpretation of PCF in the category of complete ultrametric spaces and ...
- 32.9k
49
votes
7
answers
8k
views
What constitutes denotational semantics?
On a different thread, Andrej Bauer defined denotational semantics as:
the meaning of a program is a function of the meanings of its parts.
What bothers me about this definition is that it doesn't ...
- 2,717
39
votes
7
answers
10k
views
Books on programming language semantics
I've been reading Nielson & Nielson's "Semantics with Applications", and I really like the subject. I'd like to have one more book on programming language semantics -- but I really can get only ...
- 992
12
votes
1
answer
479
views
In domain theory, what can the extra structure present in metric spaces be used for?
Smyth's chapter in the handbook of logic in computer science and other references describe how metric spaces can be used as domains. I do understand that complete metric spaces give unique fixed ...
- 891
12
votes
3
answers
1k
views
What is a good Category Theory-Domain Theory dictionary?
When dealing with the domain theoretic categories (say CPO and $\omega$CPO), I frequently wish for a dictionary for the language of category theory in domain theory.
That is, given a concept, say ...
- 2,717
25
votes
2
answers
1k
views
What is the folk model of linear logic?
Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less).
But there's a ...
- 32.9k
13
votes
0
answers
269
views
Generalizing limit-colimit coincidence to Scott-continuous adjunctions: any uses?
In Abramsky and Jung's 1994 handbook chapter on denotational semantics, after proving that the limit and colimit of expanding sequences exist and coincide, they have the following to say about ...
- 32.9k