Questions tagged [semantics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
47 votes
7 answers
7k 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 ...
user avatar
  • 2,637
36 votes
7 answers
8k 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 ...
user avatar
  • 962
28 votes
4 answers
2k views

Why do we need formal semantics for predicate logic?

Consider this question solved. I will not pick a best answer as all of them have contributed to my understanding of the topic. Im unsure what benefit we have by formally defining the semantics of ...
user avatar
  • 289
21 votes
2 answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
user avatar
  • 1,122
20 votes
5 answers
1k views

Compiler correctness proofs

I am looking for tutorial material that covers compiler correctness proofs, preferably using denotational methods, at the level of a beginning grad student. Alternatively, do you know of some ...
user avatar
  • 4,676
19 votes
4 answers
2k views

How are side effects handled in semantics?

In Anthony Aaby's "Introduction to Programming Languages" section on Semantics, he makes the following observation: Much of the work in the semantics of programming languages is motivated by ...
user avatar
  • 2,213
18 votes
4 answers
995 views

How are imperative languages more different from each other than functional languages?

I'm reading Simon Peyton Jones's The Implementation of Functional Programming Languages and there's one statement that surprised me a little bit (on page 39): To a much greater extent than is the ...
user avatar
  • 397
17 votes
3 answers
887 views

Formal Semantics of Programming Languages

I'm new to programming languages theory and I'm seeking for a good resource on a resource for formal semantics of programming languages. Specifically looking for structural operational semantics. I ...
user avatar
17 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 ...
user avatar
16 votes
3 answers
739 views

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings? I have asked some implementation issues on stackoverflow, which is not suitable ...
user avatar
  • 619
16 votes
3 answers
1k views

When can we say that two programs are different?

Q1. When can we say that two programs (written in some programming language like C++) are different? The first extreme is to say that two programs are equivalent iff they are identical. The other ...
user avatar
  • 3,993
13 votes
2 answers
496 views

What are the equational laws for zero types?

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory. In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator: $$\frac{\...
user avatar
  • 2,637
13 votes
0 answers
250 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 ...
user avatar
12 votes
1 answer
442 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 ...
user avatar
  • 791
11 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 ...
user avatar
  • 2,637
11 votes
1 answer
576 views

What exactly does "semantically observable" side-effect mean?

I have question regarding pure functions. According to the Wikipedia page one of the requisites for a pure function is : Evaluation of the result does not cause any semantically observable side ...
user avatar
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 ...
user avatar
  • 2,685
10 votes
2 answers
625 views

What's the difference between reduction strategies and evaluation strategies?

From the evaluation strategy article on Wikipedia: The notion of reduction strategy in lambda calculus is similar but distinct. From the reduction strategy article on Wikipedia: It is similar ...
user avatar
  • 281
10 votes
1 answer
216 views

Program Minimization

Circuit Minimization is the problem to minimize the size of a given circuit. Is there anything similar for general programs? In particular my question is - Do there exist algorithms to minimize the ...
user avatar
  • 1,291
10 votes
2 answers
1k views

Certified compiler and optimizations in Coq/Agda

I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For ...
user avatar
  • 443
9 votes
2 answers
1k views

Formal Definition/counter part in mathematics for “Objects” of Object Oriented Models

This is a question I asked in mathematics SE forum, and I was referred here. So here is the question- I'm a newbie in both formal mathematics and theoretical computer science, so please bear with me ...
user avatar
8 votes
4 answers
260 views

Early References for Transition System Semantics of Programs

I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of ...
user avatar
  • 12.3k
8 votes
2 answers
361 views

What's the categorical semantics of definitional equality?

The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ...
user avatar
  • 923
8 votes
2 answers
433 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 ...
user avatar
  • 235
8 votes
3 answers
393 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
user avatar
8 votes
2 answers
285 views

Where can I find an elementary small-step structural operational semantics for closures?

Lexical closures are an implementation technique in languages with first-class functions. I'm interested in a simple operational description of function closures. Does anyone know of such a ...
user avatar
  • 2,637
8 votes
2 answers
379 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. ...
user avatar
7 votes
1 answer
97 views

Semantic read-back of sharing graphs

A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used ...
user avatar
7 votes
0 answers
127 views

Are the non-lazy / non-weak semantics of the $\lambda$-calculus related to weak evaluation?

Vague question The most common semantics of the call-by-name $\lambda$-calculus (Hyland/Wadsworth’s observational equivalence $\approx_\text{HNF}$ and Morris’s observational equivalence $\approx_\text{...
user avatar
  • 521
7 votes
0 answers
124 views

Halting problem for finitary PCF

Is the halting problem decidable for finitary PCF? By "halting problem" I mean the problem of deciding whether a closed PCF term evaluates to bottom under the denotational semantics of PCF. ...
user avatar
  • 71
7 votes
0 answers
253 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 ...
user avatar
  • 179
7 votes
0 answers
339 views

The semantics of Parsing Expression Grammars

Is there a simple and intuitive explanation for the fact that the following parsing expression (where S is the starting symbol, $...
user avatar
  • 81
6 votes
2 answers
120 views

Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty ...
user avatar
  • 1,125
6 votes
1 answer
2k views

How can I prove formally semantic equivalence of programming languages?

I would like to compare two languages which are from different programming paradigms. Both langauges are object oriented languages, but one of them a multiparadigm language because it supports ...
user avatar
  • 163
6 votes
1 answer
341 views

Standard reference for basic model theory definitions

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...
user avatar
  • 203
6 votes
4 answers
7k views

Difference between syntax and semantic error in programming languages

When compilers generate errors for a specific programming language, there's distinction between syntax & semantic errors. E.g. ) + f 3 has ill-formed syntax, ...
user avatar
  • 171
6 votes
1 answer
432 views

Semantics of concurrent languages

I've seen that the preferred way to specify the semantics of a concurrent language is to use a process calculus (e.g. pi calculus, join calculus). But in the paper presenting the F# asynchronous ...
user avatar
  • 161
5 votes
2 answers
730 views

Formal representation of algorithm using recursive algebraic data types

I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this: data Data = A Int | B Data | C Data Now I am ...
user avatar
  • 211
5 votes
1 answer
158 views

Is there a notion of "inevitable reduction?"

I was just working on a semantics paper and realized I needed a notion of inevitable reduction. I came up with this definition: Let $\rightarrow$ be a binary relation. We say that $a$ inevitably ...
user avatar
5 votes
1 answer
179 views

What is a 'free model'?

I was reading this paper on effect handlers and got hung up on the phrase 'free model'. In context: [...] From an algebraic point of view, the $x_e$ provide a model for the theory of ...
user avatar
  • 605
5 votes
0 answers
95 views

Which computational models support bigotous programs?

A bigotous program is a program which decides if its input is semantically equivalent to itself. Of course, this is impossible in a Turing complete language due to Rice's theorem. In fact, its pretty ...
user avatar
  • 471
5 votes
0 answers
235 views

What's the connection between these two categories of games and innocent strategies?

Lately I've been reading a lot about game semantics and in particular the problem of PCF's full abstraction. I'm trying to understand how the definition from this article relates to the one found in ...
user avatar
  • 151
5 votes
0 answers
258 views

Is there a Galois correspondence between a Haskell class hierarchy and its instance hierarchy?

Can we consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)? In the example below the specification of the class ...
user avatar
  • 179
4 votes
3 answers
389 views

Semantic distance between excerpts of text.

I'm wondering how far along the natural language processing is in determining the semantic distance between two excerpts of text. For instance, consider the following phrases Early this morning I ...
user avatar
4 votes
3 answers
549 views

What applications of Cantor space are there?

Are there well-established applications of the Cantor space ($2^\omega$) in computer science, other than those connected with computable real arithmetic? John Tucker's page Computation on Topological ...
user avatar
4 votes
2 answers
275 views

Density of semantics in syntax

Let $L$ be a programming language, and $\cong$ a notion of equality of $L$-programs (in general $\cong$ will be undecidable). Let $syntax(n)$ be the number of $L$-programs of size $n$ (for some ...
user avatar
4 votes
1 answer
104 views

"Operations" in category theory that are not defined for arrows

Functors in category theory are defined for both objects and arrows. Depending on how they treat arrows, functors are characterized as either covariant or contravariant. Some "operations" ...
user avatar
  • 41
4 votes
2 answers
626 views

What does the category of RDF models look like in Institution Theory?

The Question in short Here is the question in its pure form. Details of my reasoning can be found below. The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of ...
user avatar
4 votes
0 answers
103 views

Origin of simulation relations for compiler correctness

Leroy uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step ...
user avatar
4 votes
0 answers
430 views

Is there a model theory for Haskell type classes?

I am trying to understand the semantics of Haskell’s type classes (TCs) from a model-theory point of view. It might difficult to give precise model theoretic semantics to type classes (see 1, and 2). ...
user avatar
  • 179