Questions tagged [semantics]

Semantics formally describe the meaning of some syntax.

35 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
8
votes
0answers
284 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 ...
6
votes
0answers
160 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. ...
5
votes
0answers
81 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 ...
5
votes
0answers
396 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 ...
4
votes
0answers
122 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
61 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 ...
3
votes
0answers
48 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 ...
3
votes
0answers
565 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 ...
3
votes
0answers
116 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 ...
3
votes
0answers
48 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, ...
3
votes
0answers
46 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 ...
3
votes
0answers
60 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 ...
2
votes
0answers
21 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 ...
2
votes
0answers
17 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 ...
2
votes
0answers
26 views

Formal semantics of a mutable/imperative stack

When introducing formal semantics for data structures, immutable stacks are a nice simple example : $\mathit{is\_empty}(\mathit{create()})=\mathrm{True}$ $\mathit{is\_empty}(\mathit{push}(e, s))=\...
2
votes
0answers
54 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 ...
2
votes
0answers
60 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$ ...
2
votes
0answers
68 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
150 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 ...
2
votes
0answers
37 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. ...
2
votes
0answers
40 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, ...
2
votes
0answers
187 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),...
1
vote
0answers
118 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 ...
1
vote
0answers
29 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 ...
1
vote
0answers
83 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....
1
vote
0answers
35 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?
0
votes
0answers
52 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?
0
votes
0answers
14 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 ...
0
votes
0answers
72 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 ...
0
votes
0answers
23 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 ...
0
votes
0answers
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 ...
0
votes
0answers
155 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'}{...
0
votes
0answers
34 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 ...
0
votes
0answers
41 views

How to check if two program are simulated or bisimulated?

Suppose I have programs A and B defined in this way: ...
0
votes
0answers
172 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 ...