# Tag Info

12

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer. Full completeness: "Sound and complete" is a ...

10

The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest. In the past few years there has been a very active line of research around so-called quantitative denotational semantics of linear logic, based on the idea (...

8

Makoto Takeyama and I sent the following to data-refinement@etl.go.jp on Jan 5, 1996: Subject: what is a data refinement relation? Dear all: anyone still interested in data refinement? Recently Mak and I have been looking again at an idea we considered many months ago. The motivation is to characterize the logical relations relevant to ...

7

Most people avoid giving precise descriptions of what a syntactic category is, because if you do it properly with all the details, the ratio of insight to necessary mathematical sophistication ends up being very, very low. John Reynolds' book Theories of Programming Languages has one of the more comprehensive explanations in its chapter 1, as does Robert ...

6

The second paragraph of Plotkin's 1973 Memo on Lambda-definability and Logical Relations says this: "The definition of logical [relation] is derived from a corresponding one of M. Gordon for the typed λ-calculus." This doesn't say explicitly that the term was coined by Gordon. But, given that the memo is titled "Lambda-definability and logical ...

6

The only natural condition I can think of is Berry's "I condition" (, Sect. 12.3): (I) each compact element dominates finitely many elements. The above condition is the defining property of Berry's dI-domains, which are distributive (that's what the "d" stands for) algebraic domains satisfying condition I. This is a widely known and well studied class ...

5

As it turns out, the OP is interested in the specific case of the interval domain. Martín Escardó's PhD thesis "PCF extended with real numbers: a domain-theoretic approach to higher-order exact real number computation" extends the programming language PCF with a datatype of reals whose denotation is the interval domain.

5

Summary: full completeness means that the interpretation function is not just complete, but also surjective on programs. Full abstraction has no requirement for surjectivity. $\newcommand{\semb}{[\![ #1 ]\!]}$ Details: The detailed meaning of full abstraction and full completeness depends on the nature of what/where/how you are interpreting. Here is a ...

4

With only flat domains, you cannot define limits to construct "infinite" structures, such as looping structures, for data or for programs. Fixpoint constructions in denotational semantics (since you used that tag) use non flat domains. Maybe you should give examples of domains that are taken as flat, while it would be better to do differently. Many problems ...

4

The comment below is correct, but it's important to understand the meaning of "finite" or "compact" elements of a domain. These are the denotations of objects computable in finite time, so their appearance in a semantic model is not for proof-theoretic convenience - they represent the strong connection between the model and actual computation.

4

[My apologies for writing this as an answer, despite the fact that it is basically just a comment to the previous answer. But I am not allowed to post a comment up there, since I do not have enough "reputation"] The previous answer is not correct. Linear logic (as well as any of its substructural systems: MLL, MALL, MELL, ALL, whatever you want...) is ...

4

Non-monotonic logic is kind of a wide area -- do you have any particular logics in mind? Anyway, defeasibly assuming :) that you are interested in any logic in which the principle of monotony fails, and you want a categorical semantics in the sense of categorical proof theory (rather than, say, a hyperdoctrine semantics), then one answer is that you can ...

4

What I am writing is essentially contained in babou's answer. But I wanted to express it a bit differently emphasizing the point of defining formal semantics. A formal semantics is a mapping from one class of mathematical structures $P$ (e.g. programs in a programming language) to another class of mathematical structure $S$ (e.g. domains): $[[ \cdot]] : ... 4 I would like to add two books not found on the answers given up to now: Aaron Stump, Programming Language Foundations David Schmidt, Denotational Semantics: A Methodology for Language Development Stump's book is concise but very clear. 4 The textbook that might be most relevant to your question is Principles of Program Analysis by Nielson, Nielson and Hankin. It does cover dataflow analysis and its relationship to denotational semantics. It does not deal with axiomatic semantics though. 4 I never found an explicit definition either, but I have inferred the folowing. As I understand, you split the language into syntactic domains; with the addition that syntactic domains must be fully generated by single different symbols, when you write down the grammar. So a syntactic domain is a subset of your language, and each domain is generated by one ... 3 (This is an extended comment). I may be misreading your definitions, but it seems to me that the relation you introduce, let us call it$\simeq$, is not an equivalence relation because it is not transitive. If$V_1,V_2$are two distinct closed normal forms (values), then obviously$V_1\not\simeq V_2$. On the other hand, the genericity lemma (Proposition ... 3 For a complete beginner studying operational semantics, I would suggest Programming Languages and Operational Semantics by Maribel Fernández. Everything is explained in a very simple manner which is easy to understand. http://www.springer.com/computer/swe/book/978-1-4471-6367-1 3 For what concerns the use of non-flat domains, babou already gave examples. I can add that sometimes it may even be useful to see integers as streams: there's ⊥, above which there are 0 and S⊥, above the latter there are S0 and SS⊥, and so on. I know that in the early 90s Loïc Colson worked on models using the above interpretation of integers, although I ... 2 Well, Mislove's quote already contains a positive answer: the category of dcpos is carteisan closed and also closed under the probabilistic powerdomain. It can indeed be used to give a denotational semantics to higher-order probabilistic computation. However, dcpos fail to satisfy the "usual approximation assumptions" that every element can be approximated ... 2 This new version of the answer tries to take into account the changes in the question, and the information exchanged in the comments. This answer assumes that$S$should be the set of variables that have a content that is used in some defined fragment of the program, rather than, at some point in the program, the variables with a content that will be ... 2 "Meaning", or "semantics" to use the more technical term, is only the understanding you wish to associate with the text of the program. It can be a mathematical function that specifies abstractedly what the program computes (denotational semantics), or it can be a formal description of how the computation is conducted by a formally defined machinery (... 2 Restating the definition to make the quantifiers easier to understand: A molecule is a finite stable approximable mapping, such that there exists a largest pair$(a,p) \in m$, such that for all other pairs$(b,q) \in m$we have$b \subseteq a$and$\{p\} \vdash q\$. In other words, a molecule is a mapping that closes off neatly, having a largest pair.

2

Got the answer, thanks to jonsterling on reddit for the insight. The error is that both M and N written as full judgements, must be weakened to have the same environment, and one that fits C[-]. So the question becomes whether ⟦M⟧ = ⟦x,y ⊢ x⟧ and ⟦N⟧ = ⟦x,y ⊢ y⟧ are observationally equivalent. And the contradiction above disappears.

1

Firstly, in addition to the Standard from 2002, there is also Technical Corrigendum 1 (TC1) from 2007 which fixes a number of issues. I don't know of any combined document. Both documents are available free of charge and links to them are available on the Z notation Wikipedia page. However, for this particular question, TC1 is not relevant. Section 15 ...

1

There are two aspects of correctness: one is internal consistency, so that whatever you define can be assigned a proper meaning. Typically, that is why you are told that the domains you use must be CPO, so that you can have limits used to defined the semantics of some looping/recursive construct, whether program or data. the other is consistency with you ...

Only top voted, non community-wiki answers of a minimum length are eligible