Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [semantics]

Semantics formally describe the meaning of some syntax.

0
votes
0answers
19 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
17 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
26 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
16 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
40 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 ...
4
votes
1answer
262 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
82 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)...
4
votes
0answers
50 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
101 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 ...
2
votes
1answer
97 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
74 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
18 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
0answers
20 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; ...
0
votes
0answers
24 views

What is an intuitive way to understand the definition of Curry and Uncurry in Categorical Language?

I was studying the definition of currying and uncurrying using Category Theory from these slides. The answer and the proof on slide 19 makes 100% sense to me however, the definitions seem to come out ...
1
vote
2answers
64 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
112 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
49 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
21 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
26 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
82 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
70 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
46 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
148 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
57 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
419 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
82 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
59 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
94 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 ...
11
votes
3answers
328 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
274 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
231 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
123 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
66 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....
7
votes
1answer
189 views

Difference between row-polymorpism and bounded polymorpishm?

I recently came across this blog post by Brian McKenna explaining row polymorphism. This seemed like a wonderful idea to me, but then I realized it smells an awful lot like bounded parametric ...
-1
votes
1answer
92 views

Meaning of “call by reference”

Can someone explain to me in a plain English what call by Reference mean ? I am having trouble to recognize a difference between "call by value" and "call by reference" Thank you.
2
votes
1answer
658 views

Semantic natural language processing - from texts to logical expressions? Universal knowledge base?

My question is - is there a semantic natural language processing that tries to understand the meaning of the texts and that tries to derive the consequences of the understood meaning? Is there a ...
3
votes
1answer
169 views

Meaning of $\triangleright$ in programming language semantics

What does the symbol "$\triangleright$" mean programming language semantics? I've seen it in the context of datatypes in and the evaluation of expressions in environments. For example : $$tenv \...
4
votes
2answers
2k views

What does it mean to “strengthen the precondition and weaken the postcondition” in Hoare logic?

Having learned a rough summary of Hoare logic (i.e. learning just the basic concept of Hoare triples and a few of the rules) I kept seeing a statement along these lines: The rule of consquence ...
4
votes
1answer
66 views

Programming Symbols : Instance/Instantiation

Is there a generally accepted symbol for indicating instantiation. That is indicating an object is an instance of a class. My first guess is to use a left arrow with a double or triple line but this ...
11
votes
1answer
147 views

Programming language semantics prototyping tool

Is there any tool for prototyping a programming language semantics and type system and that also allows for some sort of model checking of standard properties, like type soundness? I'm asking this, ...
2
votes
1answer
87 views

Collection of inference rules viewed itself as a judgment

I'm confused about the intended meaning of the following passage from Bob Harper's Practical Foundations for Programming Languages: A collection of rules is considered to define the strongest ...
7
votes
2answers
209 views

Is Semantic Preservation Soundness (or Correctness) or Completeness

When transforming terms from one language to another, the intuitively desired property is the preservation of semantics (as used e.g. here for a CPS transformatation): $$ s \Downarrow v \implies c(s) ...
4
votes
2answers
105 views

Is structural induction on terms applicable when a function is involved?

Assume an evaluation-relation on terms $t \Downarrow v$. If I want to prove correctness of a function $\phi$ w.r.t. evaluation, I have to show that the following implication always holds: $$\frac{\...
3
votes
2answers
664 views

Quantifiers in lambda calculus

I'm learning lambda calculus, however I'm quite confused about the quantifiers in lambda calculus. As far as I know, quantifiers such as "∃" are concepts of first order logic (FOL), which are not ...
3
votes
1answer
93 views

What kind of formal semantics can describe HTML and CSS?

What kind of formal semantics can describe HTML and CSS? Are there endeavours to do this. HTML/CSS layouts are espcially complex, so formalization can be of help.
6
votes
1answer
46 views

When would one use equational dynamics?

I'm trying to sort out in my mind the different ways of assigning semantics to a programming language. There are two main methodologies: operational semantics and denotational semantics (I asked a ...
6
votes
0answers
143 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. ...
14
votes
2answers
336 views

What questions can denotational semantics answer that operational semantics can't?

I am familiar with operational semantics (both small-step and big-step) for defining programming languages. I'm interested in learning denotational semantics as well, but I'm not sure if it will be ...
3
votes
0answers
105 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 ...