Semantics formally describe the meaning of some syntax.

learn more… | top users | synonyms

0
votes
0answers
19 views

LaTeX template for Semantics [closed]

Is there a LaTeX template available for Sturctural Operational Semantics (SOS) or Natural Semantics (NS)? I could not find this. Examples can be found here: ...
0
votes
1answer
131 views

What is pass-by-value-result and its advantage and disadvantage? [duplicate]

I have searched on Google, but I can't quite understand what is pass-by-value-result. What is the advantage and disadvantage of using pass-by-value-result? If I have a program code like this, what ...
3
votes
1answer
66 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 ...
0
votes
0answers
10 views

Where do I learn how to program semantic search [closed]

I want to create an archive of my many e-books and various notes (.pdf, .docx, etc.) and be able to do semantic search against that archive. Maybe something like ElasticSearch could be the archive. ...
0
votes
2answers
43 views

Rule induction principles in Harper's PFPL

I have a few small questions about section 2.4 ("Rule induction") in Practical Foundations for Programming Languages (p. 19). (1) In the rule induction principles for ...
0
votes
1answer
39 views

Is it possible to have 2 languages with different syntax but the same semantics? [closed]

I have two questions Is it possible to have 2 languages with different syntax but the same semantics? If not why not else give an example of 2 languages . Is it possible to have 2 languages with ...
2
votes
1answer
35 views

Axiomatic Semantics and Postconditions

I'll preface this by saying that this IS a homework question. However, when asked about how to solve it in class, (I believe) my professor was unable to complete it. The question is: Compute ...
4
votes
1answer
179 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 ...
3
votes
2answers
106 views

Double, down facing arrow in operational semantics

What is the meaning of the double, down facing arrow $\Downarrow$ in the context of operational semantics? Here's the example formula that uses it: $$\frac{s_0 \vdash M_1 \Downarrow P_1, s_1 \; ... ...
3
votes
0answers
47 views

How to prove that the composite strategy is prefix-closed and respects the alternation condition?

I'm doing some research on game semantics using these notes. Currently I'm trying to prove that the definition of composite-strategy is indeed a strategy. I have already proved all the conditions of ...
0
votes
0answers
41 views

Reference introductory books or articles to Game Semantics

Where can I find introductory books, articles, notes or slides on Game Semantics? I have searched a lot on the internet but I'm not satisfied by the material I found. It either is too informal, or it ...
1
vote
1answer
170 views

Is lambda calculus suitable for expressing semantics of non-functional languages?

Would it be convenient to express semantics of imperative languages (e.g. C) and object-oriented languages (e.g. Java) with $\lambda$-calculus? Or in the other words: is $\lambda$-calculus a suitable ...
2
votes
3answers
225 views

Can we create recursive functions only by using if-else statements?

I have to show whether a program containing only if-else statements but no loops is able to calculate the following type of functions: $f^n(x)$. The function $f$ is applied $n$ times to $x$, so I ...
3
votes
3answers
220 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
49 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: ...
5
votes
2answers
146 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
75 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
73 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
95 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
107 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
84 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
146 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
101 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
333 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
266 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
76 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
2k 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
494 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
83 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
239 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
199 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 ...
7
votes
1answer
200 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 ...
5
votes
1answer
35 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
87 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 ...
11
votes
2answers
280 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
212 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
239 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 ...
11
votes
4answers
309 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 ...
13
votes
2answers
359 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
308 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 ...
9
votes
2answers
312 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
123 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,$ $$ ...
10
votes
3answers
618 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
161 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 ...
8
votes
3answers
251 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 ...