Semantics formally describe the meaning of some syntax.
3
votes
3answers
127 views
What is a sort in Programming Language Semantics?
I've started reading Practical Foundations for Programming Languages and in the first chapter, the author mentions that ast's are associated with sorts. Intuitively, sorts are like types, but I'd like ...
2
votes
0answers
30 views
The grammar of the GeoQuery language
GeoQuery is a dataset used for benchmarking semantic parsers. It contains 880 queries about USA geography. The queries are in Prolog format, for example:
...
4
votes
2answers
78 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" ...
4
votes
2answers
53 views
How does one deduce small step operational semantics?
This question arises from my reading of "Types and Programming Languages" (WoldCat) by Benjamin C. Pierce.
For the small step operational semantic evaluation rules for the arithmetic expressions (NB) ...
1
vote
2answers
49 views
Proving non-confluency and adding an equation to make it confluent and terminating
I currently have a system that has {f(a) = b, f(f(x)) = x} (part of an exam question - look at page 5 - exercise 1).
To start off with proving non-confluency, I am ...
5
votes
2answers
85 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:
...
1
vote
3answers
87 views
Expressing semantics of an array as a function
An assignment questions asks the following:
Consider an array 'var a : array[1..10] of real'. Express the
semantics of this array as a function, defining the domain and
codomain (you might ...
2
votes
1answer
44 views
Homomorphisms and isomorphisms in an equational calculus
Suppose we have an algebraic specification in the form: $\{S,F,w\}$ where $S$ are the sorts, $F$ are the functions and $w$ are the set of equations.
For example, the specification for natural numbers:
...
0
votes
1answer
86 views
Initial Algebra example
If the definition of Initial Algebra is:
"An object is initial if there exists a unique morphism from the object to every
object in the category"
Why do we need such object, and could any one give ...
2
votes
2answers
96 views
Present syntax rules in a more succinct way
I am resuming syntax rules for a small language:
\begin{eqnarray*}
e_C &::=& \epsilon \mid constant \\
\textit{prefix-op} &::=& - \\
\textit{infix-op} &::=& + \mid - \mid * \\
...
3
votes
1answer
85 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 ...
7
votes
3answers
189 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 ...
1
vote
1answer
48 views
How to modify semantic actions when removing left-recursion from a grammer
Is there any algorithm that tells us how to modify semantic actions associated with a left-recursive grammar? For example, we have the following grammar, and its associated semantic actions:
$ S ...
5
votes
3answers
410 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
1answer
183 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 ...
5
votes
1answer
60 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 ...
4
votes
2answers
111 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 ...
4
votes
1answer
120 views
Looking for a simple example of Transition Semantics
I want to define a semantics of a DSL through transition semantics. For my DSL I defined the syntax and implemented a code generator. Although I can provide a demo by giving examples, I want to write ...
6
votes
1answer
152 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 ...
4
votes
1answer
28 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 ...
2
votes
1answer
59 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 ...
10
votes
2answers
204 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 ...
2
votes
2answers
162 views
Equality testing of arrays and integers in a procedural language
In terms of references and their implementation on the heap and the stack, how is
equality testing for arrays different from that for integers?
This is to do with Java programming, if you have a ...
4
votes
3answers
144 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 ...
8
votes
4answers
256 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 ...
10
votes
2answers
267 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 ...
9
votes
1answer
196 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 ...
8
votes
2answers
159 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$
...
5
votes
1answer
99 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,$
$$
...
9
votes
3answers
355 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 ...
5
votes
1answer
140 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 ...
7
votes
3answers
176 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 ...
