Questions tagged [semantics]

Semantics formally describe the meaning of some syntax.

36 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
8 votes
0 answers
344 views

Type-classes for type inference

I'm creating a semantic analyzer with type inference. For the basics I've got a type variable and a type construct with name and a list of types. I want to support overloading and I know that Haskell ...
Peter Lenkefi's user avatar
6 votes
0 answers
486 views

How are observational equivalence, contextual equivalence, and extensional equality related?

First, some context: I'm reading this blog post by Andrej Bauer. So, I stumbled in these terms: "observational equivalence" and "contextual equivalence". I know almost nothing about operational ...
Rafael Castro's user avatar
6 votes
0 answers
172 views

Is there relation between K-Framework and structural operational semantics?

K-framework strives to give one (instead of two - operational and denotational) semantics for industrial programming languages. The same unification is done by structural operational semantic as well. ...
TomR's user avatar
  • 1,381
5 votes
0 answers
131 views

What is a "model" of lambda calculus?

I know about the concept of the "model" of a logical proposition in the context of mathematical logic: It is a mathematical structure in which that proposition is true. However, it's not clear to me ...
user56834's user avatar
  • 3,692
4 votes
0 answers
139 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 ...
Michael Chav's user avatar
3 votes
0 answers
91 views

Semantics of "write-once" variables for complex data structures

Question My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus. Ideally, you give me a ...
phipsgabler's user avatar
3 votes
0 answers
52 views

Formal basis for "peephole reasoning" about code

The approaches I've seen to abstractly talking about the semantics of a programming language like Turing machines, various lambda calculi, and Hoare logic seem to be talking about the behavior of ...
Greg Nisbet's user avatar
3 votes
0 answers
734 views

How to decide between operational, denotational, and axiomatic semantics?

Context I'm designing a language which implements lambda calculus and (first-order) predicate calculus, where lambdas behave as the abstraction encapsulating logic, compositionally forming a ...
Phizo's user avatar
  • 51
3 votes
0 answers
133 views

What is the semantic model of types?

By reading literature on (denotational) semantics of types, I see that people tried to give several models of types. Reynolds showed that types in general cannot be given a set semantics in classical ...
zpavlinovic's user avatar
  • 1,644
3 votes
0 answers
53 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, ...
babou's user avatar
  • 19.4k
3 votes
0 answers
60 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 ...
Komi Golov's user avatar
3 votes
0 answers
62 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 ...
Bakuriu's user avatar
  • 807
2 votes
0 answers
38 views

Why process algebras à la chemical abstract machine are not common?

I recently read the Berry and Boudol's chemical abstract machine [1, 2]. I found the way they describe the semantic really nice and quite intuitive for a process calculus. The aspect that really ...
Bromind's user avatar
  • 121
2 votes
0 answers
23 views

How “logic-based symbolic reasoning” and “ontology” are related?

I have a basic understanding of knowledge representation systems, semantic networks and ontologies. But I can not relate my understanding to the reasoning. How the reasoning is applied on ontologies ...
Adel's user avatar
  • 121
2 votes
0 answers
56 views

Semantic/DRT methods for conversational agents / chatbots / dialogue systems - reference request?

The wiki pages about chabots mention that statistical methods, keyword search and precompiled answers are used for the chatbots. But I feel that there should exist different - semantical approach for ...
TomR's user avatar
  • 1,381
2 votes
0 answers
65 views

Select/Barrier statements in $\pi$-Calculus denotational semantics

A select statement waits on $n$ channels until channel $0$ or $1$ or ... or $n-1$ have data. A barrier lock waits on $n$ ...
Larry B.'s user avatar
  • 193
2 votes
0 answers
71 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: ...
user2411290's user avatar
2 votes
0 answers
155 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 ...
Mr. D's user avatar
  • 121
2 votes
0 answers
45 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. ...
Bakuriu's user avatar
  • 807
2 votes
0 answers
43 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, ...
Wandering Logic's user avatar
2 votes
0 answers
213 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: answer(A,longest(A,(river(A),traverse(A,B),...
Erel Segal-Halevi's user avatar
1 vote
0 answers
18 views

Rationale behind prefix-closure in CSP trace semantics

I'm currently studying Hoare's "Communicating Sequential Processes" (1) and I've come across a concept that I find a bit puzzling. In CSP trace semantics, a process's semantics are described ...
nasosev's user avatar
  • 111
1 vote
0 answers
205 views

Small step vs big step semantics for static analysis?

To be an honest question poster I do not yet fully grasp the difference between small step and big step semantics. There was a good discussion here My question is if I were to do static analysis on ...
John Smith's user avatar
1 vote
0 answers
31 views

Evaluation semantics: reduction rule for a split statement

Assume a language with statements such as $x := e$, $\text{assume}(e)$, etc., and particularly a $\text{split}\ stmt_1 ... stmt_n$ statement, constructed from $n$ statements. Informally, the semantics ...
Romain Beguet's user avatar
1 vote
0 answers
101 views

What is difference between LAG (Left Atrributed Grammar) and LATG (Left Attributed Translation Grammar)?

I am reading Compilers and am unable to understand difference between these two terms. I could not find any text which has clearly mentioned how they differ but these two separate terms are being used....
Abhishek Kumar's user avatar
1 vote
0 answers
39 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?
user18199's user avatar
0 votes
0 answers
24 views

Does lambda calculus become covariant if you fix the base type instead of the lambda calculus term?

In category theory, we are taught that polymorphic functions correspond to dinatural transformations, a k a multivariant natural transformations between functors of mixed variance $\operatorname{G} \...
Johan Thiborg-Ericson's user avatar
0 votes
0 answers
147 views

What does it mean by putting (\alpha-\beta) in front of the authors of a paper

When I was searching the publication list of some CS researchers, I sometimes saw them putting a ($\alpha-\beta$) or ($\alpha-\beta$ order) in front of the authors of a paper. What does this mean?
Francis's user avatar
  • 65
0 votes
0 answers
19 views

Denotational semantics of command sequencing

Moved from cstheory.stackexchange upon request Winskel, in his book The formal semantics of programming languages, on page 58, writes: C[c0;c1] = C[c1] o C[c0] a composition of relations, the ...
Gergely's user avatar
  • 379
0 votes
0 answers
134 views

Why algebraic semantics of programming languages have died out and have not used today?

Algebraic semantics is one type of semantics that uses algebraic expressions for connecting the formal descriptions of initial and final states of some operation of some operation that is defined in ...
TomR's user avatar
  • 1,381
0 votes
0 answers
31 views

Is natural semantics a total or partial function

I have the following def's Sns : Stm → (State ֒→ State) Sns[S] = s' (if <S,s> -> s') else undefined I'm wondering if ...
nz_21's user avatar
  • 123
0 votes
0 answers
23 views

Prooving equations are non derivable in Sigma algebra

Let Σ be the signature made up from the following symbols. e: 0 arguments function (constant symbol) f: 2 arguments function g: 1 argument function Variable set Var is made up from x,y,z Let E be ...
A. Othmane's user avatar
0 votes
0 answers
226 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'}{...
alim's user avatar
  • 994
0 votes
0 answers
38 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 ...
mavavilj's user avatar
  • 579
0 votes
0 answers
44 views

How to check if two program are simulated or bisimulated?

Suppose I have programs A and B defined in this way: ...
Oper's user avatar
  • 109
0 votes
0 answers
237 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 ...
trojan's user avatar
  • 3