Semantics formally describe the meaning of some syntax.

learn more… | top users | synonyms

1
vote
1answer
32 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
55 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
238 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
15 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
45 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
32 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
41 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
24 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
50 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
32 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
85 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
44 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
29 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
60 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
147 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
85 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, ...
6
votes
1answer
400 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
31 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
132 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
174 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
27 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
43 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
198 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
55 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
0
votes
1answer
91 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
145 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
183 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
30 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
114 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
109 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
89 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
253 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
265 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
450 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
349 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
57 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
32 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
231 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
838 views
0
votes
0answers
63 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 ...