Semantics formally describe the meaning of some syntax.

learn more… | top users | synonyms

0
votes
0answers
23 views

what is the connection between evaluation context and call by value?

I been reading about $\lambda$-calculus and related stuff, but I got some confusions which i want to clarify. The call by value reduction is expressed with two rules $$ \frac{e_1 \rightarrow e_1'}{...
2
votes
1answer
43 views

What are these questions in the PoplMark challenge asking?

I was reading the paper Mechanized Metatheory for the Masses: the PoplMark Challenge by Aydemir et al (PDF) and I found the following three questions on page 13 of the PDF a bit confusing. ...
3
votes
1answer
47 views

How does recursion works when there are 2 or more consecutive recursive calls?

I was learning about recursion and i came across the following pseudo code for quicksort. ...
0
votes
0answers
11 views

how to understand these in PoPLMARK challenge? [duplicate]

I was reading the PoPLMARK challenge and in the paper proposed that challenge, I find some parts confusing me, here original paper. In challenge 3:Testing and Animating with respect to semantics, I ...
3
votes
1answer
28 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
35 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, I'...
3
votes
2answers
65 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|}\ P_1|...
5
votes
1answer
243 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
19 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
39 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
47 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
45 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
26 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
55 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
34 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
94 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
70 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
31 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
64 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
166 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
535 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
33 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
140 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
196 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
56 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
214 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
94 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
35 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
154 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
210 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
39 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
119 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
115 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
92 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
303 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
274 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
456 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
377 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
59 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 ...