Questions tagged [semantics]

Semantics formally describe the meaning of some syntax.

Filter by
Sorted by
Tagged with
36 votes
1 answer
11k 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.
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.1k
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.1k
19 votes
2 answers
4k 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
18 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 ...
  • 71.4k
17 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 ...
  • 171
16 votes
4 answers
859 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 ...
16 votes
2 answers
608 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,190
14 votes
2 answers
930 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$ ...
  • 711
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
529 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
936 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" ...
  • 253
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 ...
  • 71.4k
11 votes
1 answer
205 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, ...
10 votes
2 answers
926 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? ...
  • 409
10 votes
2 answers
473 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 ...
10 votes
1 answer
143 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 ...
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
510 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 ...
  • 257
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
7k 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
324 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
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
194 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,230
8 votes
0 answers
318 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 ...
7 votes
2 answers
184 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 ...
7 votes
2 answers
970 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 ...
7 votes
2 answers
280 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
315 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,190
6 votes
2 answers
1k 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 ...
  • 1
6 votes
1 answer
5k 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 ...
6 votes
1 answer
59 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,190
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" ...
6 votes
3 answers
13k 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 ...
6 votes
1 answer
813 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
55 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: ...
6 votes
1 answer
365 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.1k
6 votes
1 answer
336 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.1k
6 votes
0 answers
169 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,351
5 votes
2 answers
872 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
1 answer
232 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,185
5 votes
1 answer
141 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,370
5 votes
1 answer
352 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
317 views

The definition of weakest precondition for a non-deterministic language

In the classical IMP language, the definition of weakest precondition is: definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" This is stating that from state s, after ...
  • 2,230
5 votes
1 answer
319 views

The importance of the language semantics for code generation and frameworks for code generation in model-driven development

I am implementing worflow where the code in industrial programming languages (JavaScript and Java) should be generated from the formal (formally verified) expressions (from ontologies as objects and ...
  • 1,351
5 votes
1 answer
2k 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 ...
5 votes
2 answers
3k views

Static scope and dynamic scope

I am perpetually confused when it comes to static scoping and dynamic scoping and their differences and Wikipedia isn't of any help, so here's my question: Given the following pseudo code in a ...