Questions tagged [semantics]

Semantics formally describe the meaning of some syntax.

Filter by
Sorted by
Tagged with
0
votes
0answers
29 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
20 views

What does this semantic specification do about shuffling a single card of a Deck?

I have 2 constructor functions and 2 additional function: declare: d,d' = deck; c, c' = card Constructor 1) CreateDeck(); ...
0
votes
0answers
13 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 ...
4
votes
1answer
96 views

What should I read to understand semantics of programming languages?

I would like to have a good conceptual understanding of the semantics of programming languages: operational-, denotational-, axiomatic-, categorical-. Is there a good (standard?) textbook for this?
0
votes
0answers
10 views

What are RDF graphs and OWLs commonly used for?

Not sure if this is the right site, but I'll give it a go. I find the concept of the Semantic Web fascinating, and the idea of using RDF triples to represent semantic data. But obviously the vision ...
0
votes
2answers
107 views

Is type-checking “syntactic” or “semantic”?

On the wikipedia page on compilers, it says: Semantic analysis adds semantic information to the parse tree and builds the symbol table. This phase performs semantic checks such as type checking (...
3
votes
2answers
269 views

Why is the assignment rule the way it is in Hoare Logic?

Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics? I can't wrap my head around why the assignment rule is backwards from what I expected. I understand Hoare logic is use to ...
1
vote
1answer
38 views

Is the problem of deciding whether two programs have the same semantics decidable?

If I have program and I want to check whether other programs have the exact same semantics or not, could I always build a machine that could make that decision? This is a question relevant to ...
9
votes
1answer
103 views

Analogue of the topology-computability correspondence for computational complexity

There is an interesting correspondence between notions of topology and notions of computability theory originating from the ingenious idea of Dana Scott to identify computable functions with ...
2
votes
1answer
38 views

What is the denotation for identifiers?

I am trying to understand what is the domain for denotational semantics. Right now the way I understand denotational semantics is that given some syntax of a program that maps to some mathematical ...
2
votes
1answer
20 views

Finding two store typings that make the same store valid (lambda-calculus with references)

Problem 13.5.2 of Pierce's TAPL's book (page 167) asks: Can you find a context $\Gamma$, a store $\mu$ and two different store typings $\Sigma_1,\Sigma_2$ such that both $\Gamma | \Sigma_1 \vdash \...
6
votes
1answer
72 views

What is meant by a full abstract model of a lambda-calculus like language?

The simply typed lambda-calculus with numbers and fix has long been a favorite experimental subject for programming language researchers, since it is the simplest language in which a range of subtle ...
2
votes
0answers
13 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 ...
0
votes
2answers
71 views

Why there is forward chaining inference engine (reasoner) for description logics only and not for other logics?

Reasoner is forward chaining inference engine (https://en.wikipedia.org/wiki/Semantic_reasoner) as opposite to Prolog backward chaining SAT solver (for queries). Why there is reasoner for description ...
0
votes
0answers
28 views

What is the difference between programming and planning? Is programming the special case of planning?

Computer programming is laying out the predefined operations (actions) in compositional/recursive/recurrent manner to go from one defined state (e.g. assignment of variables) to the other defined ...
0
votes
0answers
60 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
1answer
78 views

Do the following concepts belong to syntax or semantics?

I am not very sure about the difference between syntax and semantics. Does each of the following concepts belong to syntax or semantics? terms values: terms that are possible final results of ...
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
22 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 ...
1
vote
1answer
134 views

What is the relation between an algorithm and its implementation at the level of code?

Is there any isomorphism or equivalence relation? What strictly bind these two together?
2
votes
0answers
23 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))=\...
1
vote
0answers
96 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 ...
6
votes
1answer
2k views

What's the difference between: operational, denotational and axiomatic semantics?

Recap of the terms from the dictionary: semantics: the study of meaning in a language (words, phrases, etc) and of language constructs in programming languages (basically any syntactically valid part ...
2
votes
1answer
361 views

Negation of the semantics of the Until operator in LTL

I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to: $\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
5
votes
0answers
75 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
1answer
152 views

The definition of weakest precondition for a non-deterministic language

In the classical IMP language, the definition of weakest precondition is: definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" This is stating that from state s, after ...
3
votes
1answer
171 views

The Law of Excluded Miracle in the language of guarded commands

The definition of weakest precondition is familiar (let me use Isabelle's syntax here): definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" the weakest precondition ...
2
votes
1answer
206 views

How does one prove that Big Step semantics and Small Step semantics are equivalent for IMP?

I know there is this paper but I wanted to do a special case proof for just IMP for fun. So the theorem is: $$ \langle P , \sigma \rangle \to_{Big} \langle \{ \} , \sigma' \rangle \iff \exists N \...
0
votes
1answer
27 views

Examples of interesting semantics to study during a small project for a graduate Semantics course

I have been following the course Concrete Semantics with Isabelle/HOL. At some point we are given the task to verify a program/extend some semantic construction/prove some mathematical fact. I ...
1
vote
1answer
45 views

What are $(S,\Sigma)$-CCCs?

I was reading this and I was trying to understand the definition of $(S,\Sigma)$-CCC. The first requirement says: a mapping [[_]] : S → |C|, associating some object [[s]] ∈ |C| to any s ∈ S; ...
1
vote
2answers
112 views

How is it that programs can be identified with partial functions for programming language semantics?

I was reading about denotational semantics Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, ...
2
votes
2answers
171 views

Proving parametricity for Gallina functions

I have the following definitions Definition nat'' {X : Type} := (X -> X) -> X -> X. Definition nat' := forall (X : Type), @nat'' X. And when I wanted to ...
2
votes
1answer
72 views

How does topic or tag suggestion algorithms work?

I know it's a keyword based search. But sites like Quora have some good suggesting algorithms where the algorithm understands the intent of question asked rather than just the keywords meanings. For ...
2
votes
1answer
29 views

Unclear logic notation for PFX program rules

I'm very new to this so please bear with me. I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the ...
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 ...
1
vote
0answers
27 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 ...
3
votes
1answer
90 views

Programmatically checking equivalence of statements

So as part of a theorem-prover/checker, I'm using Prolog to try to determine the equivalence of statements that have been parsed into tree form, e.g. $x=2$ is represented as ...
4
votes
1answer
78 views

Why does substitution terminate?

I'm formalizing some properties of lambda calculus in Coq and I have some problems proving termination of substitution. My terms are defined as: ...
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 ...
7
votes
2answers
171 views

Formal model of execution for Java (or general imperative language)

I'm trying to prove some statements about execution in Java programs under some heavy restrictions (basically I have a conjecture that if two methods satisfy a set of constraints for a given input ...
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$ ...
3
votes
0answers
486 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 ...
4
votes
1answer
104 views

How to express modalities in lambda calculus - are some extensions required?

Lambda calculus can be used for encoding semantics of natural language, e.g. http://yoavartzi.com/tutorial/ contains full details about semantic parsing of natural language: converting natural ...
1
vote
1answer
72 views

I'm looking for a construct that is to semantic-analysis what NFA/DFA are to scanning and DPDA is to parsing

What maps to Semantic Analysis the way automata like Finite State Machines and Pushdown automatons map to Lexing and Parsing? A couple of years ago I came across a paper that presented such a ...
4
votes
1answer
104 views

What formal representation is commonly used to describe compiler optimizations?

I have devised a compiler optimization that works on any structured language that has arrays assignments array[index] = value and counted loops ...
13
votes
3answers
425 views

What's the difference between a calculus and a programming language?

I think I'm pretty confused about what's called a calculus and what's called a programming language. I tend to think, and might have been told, that a calculus is a formal system for reasoning about ...
4
votes
0answers
361 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 ...
8
votes
0answers
270 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 ...
0
votes
1answer
131 views

Strategy to create a testbed and gold standard

I need to create a correct evaluation of the method I'm proposing. The problem is that in the field I'm working on there is no benchmark that I can use for this purpose. On the other hand, my method ...
1
vote
0answers
74 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....