Questions tagged [semantics]
Semantics formally describe the meaning of some syntax.
179
questions
41
votes
2
answers
13k
views
Difference Between Small and Big-step Operational Semantics
What's the fundamental difference(s) between small and big-step operational semantics?
I'm having a hard time grasping what it is and the motivation for having the two.
- 513
25
votes
5
answers
1k
views
$\lambda$-calculus with reflection
I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs.
Is there an untyped $\lambda$-calculus extension that ...
- 20.2k
20
votes
3
answers
3k
views
When are two simulations not a bisimulation?
Given a labelled transition system $(S,\Lambda,\to)$, where $S$ is a set of states, $\Lambda$ is a set of labels, and $\to\subseteq S\times\Lambda\times S$ is a ternary relation. As usual, write $p \...
- 20.2k
19
votes
2
answers
5k
views
What is this fraction-like "discrete mathematics"–style notation used for formal rules?
In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules":
What is this notation called? How do I read it?
For example:
the ...
- 293
19
votes
3
answers
1k
views
Problems Implementing Closures in Non-functional Settings
In programming languages, closures are a popular and often desired feature. Wikipedia says (emphasis mine):
In computer science, a closure (...) is a function together with a referencing ...
- 72.4k
18
votes
2
answers
2k
views
Scott-continuous functions: an alternative definition
I'm really struggling with this property:
Let $X,Y$ be coherence spaces and $f: Cl(X) \rightarrow Cl(Y)$ be a monotone function. $f$ is continuous if and only if $f(\bigcup_{x\in D} x)=\bigcup_{x \in ...
- 181
17
votes
2
answers
691
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 ...
- 2,230
16
votes
4
answers
882
views
Can a program language be malleable enough to allow programs to extend language semantics
With reference to features in languages like ruby (and javascript), which allow a programmer to extend/override classes any time after defining it (including classes like String), is it theoretically ...
- 273
14
votes
2
answers
1k
views
Confluence proof for a simple rewriting system
Assume we have a simple language that consists of the terms:
$\mathtt{true}$
$\mathtt{false}$
if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$
...
- 701
14
votes
1
answer
2k
views
what is semantics?
There are many popular languages. But, computer scientists tell us that in order to understand the behaviour of programs in those languages definitely and unambiguously argue upon program behavior (e....
- 1
14
votes
3
answers
592
views
What's the difference between a calculus and a programming language?
I think I'm pretty confused about what's called a calculus and what's called a programming language.
I tend to think, and might have been told, that a calculus is a formal system for reasoning about ...
- 398
13
votes
4
answers
1k
views
Getting started with Program Analysis
I'm looking for resources on getting started with program analysis.
The only book I've found on the topic is the Nielson & Nielson book.
Other than that, it seems like there are only "compiler" ...
- 263
12
votes
2
answers
2k
views
How to deal with arrays during Hoare-style correctness proofs
In the discussion around this question, Gilles mentions correctly that any correctness proof of an algorithm that uses arrays has to prove that there are no out-of-bounds array accesses; depending on ...
- 72.4k
11
votes
1
answer
215
views
Programming language semantics prototyping tool
Is there any tool for prototyping a programming language semantics and type system and that also allows for some sort of model checking of standard properties, like type soundness?
I'm asking this, ...
- 283
10
votes
2
answers
950
views
Which fixpoint is Haskell list type?
Let's say that lists are defined as
List a = Nil | Cons a (List a)
Then, in Haskell is List x the greatest or least fixpoint? ...
- 419
10
votes
2
answers
516
views
Is there a canonical definition of “pure” function?
StackOverflow pointed me here, so the question might be a bit in a layman's terms.
Wikipedia defines pure functions as
In computer programming, a function may be described as a pure
function if ...
- 203
10
votes
1
answer
162
views
Analogue of the topology-computability correspondence for computational complexity
There is an interesting correspondence between notions of topology and notions of computability theory originating from the ingenious idea of Dana Scott to identify computable functions with ...
- 101
9
votes
2
answers
3k
views
Difference between multimethods and overloading
Context
I've been programming in java for a few years now. And atm i'm learning something totally different: Clojure.
There the expression problem can be solved by using multimethods whereas in java ...
- 215
9
votes
3
answers
553
views
Is reference counting GC vs. tracing GC a language property or an implementation property?
We sometimes hear "Swift doesn't do classic (tracing) GC, it uses ARC."
But I'm not sure if there is anything in the Swift semantics that requires reference counting. It seems that one could build ...
- 267
9
votes
4
answers
1k
views
What is a sort in programming language semantics?
In Chapter 1 of Practical Foundations for Programming Languages, the author mentions that abstract syntax trees are associated with sorts.
Intuitively, sorts are like types, but I'd like to know if ...
- 91
9
votes
1
answer
9k
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 ...
- 193
8
votes
1
answer
6k
views
What is a linearization point?
With respect concurrent programming, what is a linearization point?
They seem to occur at a compare-and-swap instruction apparently. The best definition I could find is here.
All function calls ...
- 81
8
votes
1
answer
2k
views
Lambda Calculus: How do evaluation contexts "work"
In the pure lambda calculus, we have the inductively defined set of terms (the grammar):
$$e::= x \mid \lambda x . e \mid e_1 e_2$$
Under the call-by-value evaluation strategy, we have the inference ...
- 593
8
votes
1
answer
335
views
Formally describing a new domain specific programming language
I am about to implement a domain specific language for representation of social learning conventions. Part of the implementation is a formal description of a language - its 'calculus', symbols and ...
- 297
8
votes
1
answer
259
views
What is meant by a full abstract model of a lambda-calculus like language?
The simply typed lambda-calculus with numbers and fix has long been a favorite experimental subject for programming language researchers, since it is the simplest language in which a range of subtle ...
- 2,194
8
votes
0
answers
345
views
Type-classes for type inference
I'm creating a semantic analyzer with type inference. For the basics I've got a type variable and a type construct with name and a list of types.
I want to support overloading and I know that Haskell ...
- 208
7
votes
2
answers
206
views
Formal model of execution for Java (or general imperative language)
I'm trying to prove some statements about execution in Java programs under some heavy restrictions (basically I have a conjecture that if two methods satisfy a set of constraints for a given input ...
- 387
7
votes
2
answers
1k
views
Are syntax and semantic just 2 structures such that one is a model of the other?
The syntax of a language is a structure.
The semantic of a language is a structure.
The semantic of a language is a model of its syntax.
And that's all ? The duality syntax/semantic is just model ...
- 669
7
votes
3
answers
1k
views
Inheritance, and dynamic access to members/attributes and methods in Java-like languages
I have a question about inheritance in Java-like OO programming languages. It came up
in my compiler class, when I explained how to compile methods and their invocation. I was using Java as example ...
- 8,308
7
votes
2
answers
305
views
Is Semantic Preservation Soundness (or Correctness) or Completeness
When transforming terms from one language to another, the intuitively desired property is the preservation of semantics (as used e.g. here for a CPS transformatation):
$$ s \Downarrow v \implies c(s) ...
- 610
7
votes
1
answer
359
views
Difference between row-polymorpism and bounded polymorpishm?
I recently came across this blog post by Brian McKenna explaining row polymorphism. This seemed like a wonderful idea to me, but then I realized it smells an awful lot like bounded parametric ...
- 2,230
6
votes
2
answers
2k
views
What are the axioms, inference rules, and (formal) semantics of lambda calculus?
Wikipedia says that lambda calculus is a formal system. It defines lambda calculus by giving its alphabet, and inductively describing what is inside its formal language.
Since lambda calculus is a ...
- 4,895
6
votes
1
answer
64
views
When would one use equational dynamics?
I'm trying to sort out in my mind the different ways of assigning semantics to a programming language. There are two main methodologies: operational semantics and denotational semantics (I asked a ...
- 2,230
6
votes
2
answers
1k
views
Why is there readonly (const) in C++, but not writeonly (sink)?
C++ initially had "readonly" and "writeonly" qualifiers, before "readonly" was renamed to "const", and "writeonly" removed. My question is: What are the problems with "writeonly" (or a "sink" ...
- 5,390
6
votes
3
answers
14k
views
Call by value-result vs. call by reference?
From my Googling, it appears that call by value-result is similar to call by reference in that it changes values in the caller, but it's different in that the changes don't take place until the callee ...
- 233
6
votes
1
answer
878
views
Typing dependent pattern matching
I'm curious on how to type a dependent pattern matching in a functional language. What should the rule for typing
...
- 398
6
votes
1
answer
61
views
Dynamic changes to classes or context activation -- how to treat existing objects in a consistent way?
I am looking for references and papers on the following topic.
In general, some programming languages allow dynamic changes to classes. As an example, a new instance variable ‘weight’ can be added to ...
- 661
6
votes
2
answers
111
views
Formally describing a sensor network language
I have a language for sensor networks (generates C code) and I want to define the formal semantics of it.
The language has this form:
...
- 113
6
votes
1
answer
381
views
Late and Early Bisimulation
This is a follow up to my earlier questions on coinduction and bisimulation.
A relation $R \subseteq S \times S$ on the states of an LTS is a bisimulation iff $\forall (p,q)\in R,$
$$
\begin{array}...
- 20.2k
6
votes
1
answer
351
views
Reflection on Concurrency
Reflection is a common mechanism for accessing and changing the structure of a program at run-time, found in many dynamic programming languages such as Smalltalk, Ruby and Python, and in impoverished ...
- 20.2k
6
votes
0
answers
488
views
How are observational equivalence, contextual equivalence, and extensional equality related?
First, some context: I'm reading this blog post by Andrej Bauer.
So, I stumbled in these terms: "observational equivalence" and "contextual equivalence".
I know almost nothing about operational ...
- 499
6
votes
0
answers
172
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. ...
- 1,401
5
votes
2
answers
944
views
Break keyword outside a loop is syntax error or semantic error?
I am designing a simple compiler for my university project. In my programming language, the break keyword is allowed.
I want to know whether break keyword occurs outside a loop should be a syntax ...
5
votes
3
answers
1k
views
Hoare triple for assignment P{x/E} x:=E {P}
I am trying to understand Hoare logic presented at Wikipedia,
Hoare logic at Wikipedia
Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means
if P just before C, then Q ...
- 374
5
votes
2
answers
5k
views
What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?
Having learned a rough summary of Hoare logic (i.e. learning just the basic concept of Hoare triples and a few of the rules) I kept seeing a statement along these lines:
The rule of consquence ...
- 495
5
votes
1
answer
2k
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 be ...
- 183
5
votes
1
answer
243
views
Notation for operational semantics that can be used in code comments
I'm defining an intermediate language for a multi-backend code generator that I'm writing. I want to document the operational semantics for this intermediate language in a way that is readable both ...
- 1,204
5
votes
1
answer
153
views
When are Dynamic and Lexical Scoping equivalent?
I am designing a small DSL and I know that implementing dynamic scoping (with a simple global stack) is easier then using full lexical scoping (each function needs its own scope/closure). What kind of ...
- 1,379
5
votes
1
answer
377
views
Why injection into sum type apparently leads to ambiguity?
I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that ...
- 331
5
votes
1
answer
733
views
Resources for implementing dependent type theory
I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
- 347