Semantics formally describe the meaning of some syntax.

learn more… | top users | synonyms

0
votes
1answer
17 views

Principles of Programming Languages: Understanding Judgements

I am taking a principles of programming languages class right now and am trying to understand the following judgement form. ...
5
votes
2answers
51 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? ...
2
votes
0answers
24 views

How do stable functions 1 => 1 relate to Bool?

One way to interpret the (simply typed) lambda calculus is via coherence spaces (Proofs and Types, chapter 8). For example, we can consider the space containing token element ($\mathbf{1}$) and the ...
1
vote
1answer
83 views

Semantic Code Comparison

Consider two codes that do the same thing, in the same time and memory order, But they don't do it exactly the same way. Is there any Idea for a program to declare those codes as the same? For ...
3
votes
1answer
56 views

Meaning of type inference rule for abstraction in lambda-calculus

Below is a snippet about simply typed lambda-calculus from CS152: Programming Languages Lecture 9 | Simply Typed Lambda Calculus, on printed‑page 15, indexed 23. $$ \frac {\Gamma, x: \tau_1 \vdash e: ...
1
vote
2answers
65 views

Call‑by‑name will succeeds where call‑by‑value may fails: some example cases?

I've landed to SML pages, comparing call‑by‑name and call‑by‑value, asserting the former always succeed while the latter may fails. As this seems counter intuitive to me, I feel at least an example ...
2
votes
1answer
59 views

Call by need compared to pass by function

SML uses pass‑by‑value, Haskell uses call‑by‑need. Unless I'm wrong (the purpose of this question), one can do call‑by‑need with SML, passing a function instead of a value; a function to be later ...
1
vote
2answers
130 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 ...
3
votes
3answers
422 views

Does a logical system have semantics?

From Wikipedia: A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to ...
4
votes
2answers
108 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" ...
2
votes
1answer
38 views

Is proof of totality of a semantic function for binary numbers cicular?

I think the following proof found in a textbook is circular, since the proof for case n=n'0 assumes the case n=n'1 and vice versa. Am I missing something? Proof that the semantic function N is a ...
1
vote
0answers
28 views

How to represent semantics with Combinatory Logic

How is Combinatory Logic relevant to software design? For example, can one transform programs into CL? If so, how? Does CL provide a canonical representation for programs?
2
votes
0answers
23 views

How can I talk about priority inversion if it's impossible to specify priority?

In the paper: Leslie Lamport: What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority; ACM Symp Principles of Programming Languages, (POPL-12):78-83, ...
7
votes
2answers
135 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 ...
2
votes
3answers
160 views
0
votes
0answers
41 views

Proving the small-step semantics of factorial program

I am given the following command $C$: $y:=1;$ while $\neg (x=1)$ do $y:= y*x;$ $x:= x - 1$. I have to show that $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto s(x)!\}$ if $s(x) \geq 1$ and undefined ...
1
vote
1answer
51 views

Small-step semantics: for-loops

I'm trying to construct the small-step semantic rules involving the for-loops, but I can't find anything about it in the literature (only about while-loops). I was wondering if anyone could help me ...
0
votes
1answer
596 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
120 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
16 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. ...
1
vote
2answers
65 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
62 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
42 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
231 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
152 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
54 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
45 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
185 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
353 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 ...
6
votes
4answers
284 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 ...
2
votes
0answers
66 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
163 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
93 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) ...
2
votes
2answers
78 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
98 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
110 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
92 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
210 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
104 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
502 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
312 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
82 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 ...
7
votes
1answer
728 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
90 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 ...
5
votes
2answers
381 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
240 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
216 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 ...
3
votes
1answer
106 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 ...