Semantics formally describe the meaning of some syntax.

learn more… | top users | synonyms

3
votes
1answer
26 views

What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics?

Revising for an exam and I'm trying to get to grips with operational semantics. Here's the exam question that prompted me posting this: Exam Question: We add to the language $\mathsf{SIMP}$ two new ...
1
vote
1answer
34 views

How exactly does on describe the formal semantics of the Applied $\pi$-Calculus?

In "Mobile Values, New Names, and Secure Communication", Abadí and Fournet describe thet Applied-$\pi$-Calculus. Although I understood a great part of the description of the Applied $\pi$-Calculus, ...
3
votes
2answers
63 views

Why do some authors not include summation in the $\pi$-Calculus?

In Robin Milner's book "Communicating and Mobile Systems: the $\pi$-Calculus", on page 87, the set of expressions of the $\pi$-Calculus is defined as $$P ::= \sum_{i\in I} \pi_i.P_i\ {\huge|}\ ...
5
votes
1answer
240 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 ...
2
votes
0answers
16 views

Framework of code generation in model-driven development workflow. Is formal language semantics necessary?

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 ...
2
votes
0answers
46 views

Question about Dynamic Scoping example output

I'm trying to do a runtime stack on a simple code example that uses dynamic scoping. The code is this: ...
2
votes
0answers
35 views

Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
3
votes
1answer
45 views

premiss of reduction rule (abst) of pure type systems

$$(abst) \:\frac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3}$$ In this rule, why is $(x: t_1) \to t_3$ required to be an ...
1
vote
1answer
42 views

How might I express a sequence of operations in formal terms?

I want to be able to represent a set of operations in sequential order such that they will represent what is traditionally called a "function" (which is not always the mathematical definition of a ...
0
votes
0answers
25 views

How can I extend a context-free grammar to Lexical semantics?

Here it was suggested that I may need Lexical semantics for my parsing problems. How can I extend a context-free grammar to Lexical semantics? I've thought attribute grammars already, but they seem ...
0
votes
0answers
6 views

Relationship between instance node in Semantic Network

I am trying to draw a semantic network from the description like this: Undergraduate is a student and has to attend a particular course. Lecturer is a staff and give a course. John is an ...
4
votes
1answer
51 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 ...
-1
votes
1answer
33 views

Does checking for correctness belong predominantly to “semantic analysis”?

Does checking for correctness belong predominantly to "semantic analysis"? Or is it reasonable to be done in earlier phases (in a compiler like construction) as well? Mainly in syntax analysis. Or is ...
0
votes
0answers
24 views

What semantical is there in attribute grammars?

I've been reading about attribute grammars since I'm trying to extend CFGs to semantics. What I'm finding difficult to grasp is the use of the word "semantics" in the context of attribute grammars. ...
8
votes
2answers
88 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 ...
0
votes
0answers
48 views

Possible results of two programs running on a symmetric multicore system

This question is from Patterson and Hennessy's Computer Organization and Design. Consider the following portions of two different programs running at the same time on four processors in a ...
1
vote
1answer
30 views

How to express taking the next bit of an infinite string in small-step semantics?

I have to write a rule as part of a small step operational semantics (https://en.wikipedia.org/wiki/Operational_semantics). Whenever this rule is applied, the next bit belonging to an infinite bit ...
1
vote
1answer
31 views

denotional semantic for while - fixed points

In my book it is written: $$[[\text{while b do S}]] = \text{FIX F}$$, where $Fg = cond (\beta[[b]], g\circ [[S]], id). $ What is cond ? $[[\text{if b then S1 else S2}]] = cond (\beta[[b]], [[S1]], ...
2
votes
1answer
62 views

Scientific soundness of computer science papers [closed]

First of all, this question relates to an issue that affects several areas of science, but since StackExchange doesn't have a meta science section I'll make it specific to computer science, which is ...
4
votes
2answers
161 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 ...
4
votes
0answers
87 views

Why can't a programming language be both fully recursive and polymorphic

In my theory of computation class last Spring my professor said in passing that a programming language cannot be both fully recursive and polymorphic. I didn't think much of it till now? What does it ...
3
votes
0answers
32 views

A syntactic property of computing systems: is non-coding DNA universal?

One of the surprising aspect of the genome for lay-people is that it contains important non-coding DNA parts, which does not mean that they are all useless. I never paid so much attention to the fact, ...
7
votes
1answer
451 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.
0
votes
0answers
32 views

How to check if two program are simulated or bisimulated?

Suppose I have programs A and B defined in this way: ...
2
votes
1answer
134 views

Denotational semantics of expressions with side effects

I'm doing revision for a module on programming language semantics and I'm having trouble understanding the introduction of side-effects in expressions. We assume a standard syntax for arithmetic ...
1
vote
2answers
182 views

Why are syntax trees used in genetic programming?

Reading a course on genetic programming, the first chapter describes the syntax tree as the basic representation of programs in genetic programming. What are the reasons leading to the choice of a ...
2
votes
0answers
28 views

How to prove that justice isn't enough to produce all naturals?

I'm doing the exercises from the first chapter of the book "Temporal Verification of Reactive Systems Safety" by Manna and Pnueli. However I find very difficult to solve the point c of problem 0.2. ...
1
vote
1answer
44 views

Defining function for arithmetic expressions

I've got these arithmetic expressions a ::= n | x | a1 + a2 | a1 ? a2 | a1 − a2 which are a part of language. An undefined element is allowed ⊥ ...
3
votes
1answer
61 views

Description and semantics of program graphs

I'm working on a question which gives me a program graph and tells me to give a mathematical description of it. I'm aware that a program graph PG is a tuple $(Loc, Act, Effect, \rightarrow, Loc_0, ...
2
votes
1answer
53 views

Proof via induction for small-step semantics

I'm doing a course in Computer Programming Languages and I'm trying to prove the following (roughly following Pierce's Types and Programming Languages book): if $t \rightarrow^* t'$ then $if\; t\; ...
2
votes
2answers
202 views

What do I need to study in order to understand and design a programming language? [closed]

What do I need to read in in order to : understand the specs of an already made programming language Design a programming language Design a compiler and assembler for that language make an ...
1
vote
1answer
56 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
0
votes
1answer
93 views

Why are types and grammar non-terminals so distinct?

Sorry ahead of time if some of my terminology is inaccurate, my formal training isn't quite to the level it should be. Almost all programming languages with types separate built-in functions ...
1
vote
1answer
34 views

Semantic information collections on the web. (Semantic Wikipedia)

There are lots of technologies supporting semantic information markup even as wiki software. I am wondering if there is any kind of broad information collection project like Wikipedia which features ...
0
votes
0answers
29 views

Are if statements avoidable is we define a program according to explicit state transitions? [duplicate]

This question occurred to me some time ago when I was thinking about whether or not if statements are fundamental in computation. Consider a program that manages a ...
0
votes
1answer
147 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. ...
7
votes
2answers
193 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? ...
3
votes
0answers
38 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
117 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 ...
4
votes
1answer
111 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
90 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
290 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 ...
2
votes
2answers
270 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
451 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
356 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
58 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
31 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
33 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, ...
8
votes
2answers
237 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 ...
3
votes
3answers
861 views