Questions tagged [semantics]

Semantics formally describe the meaning of some syntax.

Filter by
Sorted by
Tagged with
2 votes
1 answer
64 views

Mitchell FPL 3.6.2 (Show that equation does not hold in initial algebra)

Mitchell specifies a set data type: ie, an algebraic specification for set. He then asks to prove that the equation union s s' = union s' s [s, s': set] does not hold in the initial algebra. He ...
emesupap's user avatar
  • 173
0 votes
1 answer
32 views

Results of a Program After Call By Reference Vs. Call By Value-Result

I have a question that I am trying to work through. I have a program: ...
RDizzl3's user avatar
  • 101
0 votes
1 answer
61 views

How to evaluate an arbitrary mathematical expression

For Instance, if I allowed the user to pass in expressions like "35 + 2 * 5" as strings, how would I go about writing such a program? Also, what topics does this question fall under?
Enoch's user avatar
  • 11
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
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
0 votes
1 answer
52 views

Definition of "deterministic" semantics in While language

I came across this definition in my book but I'm not sure that I understand it correctly. Isn't this the same as saying: $\langle S, s\rangle \rightarrow s = \langle S, s\rangle \rightarrow s$ ...
Ayyware's user avatar
2 votes
1 answer
576 views

What is the definition of a redex and what are they for in programming languages literature?

I saw the word "redex" in the context of proramming language theory/semantics in 2018 and now when I was reading a neurosymbolic research paper (machine learning with neural nets + symbolic ...
Charlie Parker's user avatar
1 vote
1 answer
78 views

When is a stuck state not final and when is a maximal sequence not complete in transition systems?

Reading the book Practical Foundations for Programming Language. In section 5.1 Transition Systems, the author said that Whereas all final states are, by convention, stuck, there may be stuck states ...
chansey's user avatar
  • 285
3 votes
2 answers
126 views

Semantics and implementation of side effects

From a practical point of view, how do functional languages with formally specified semantics (like ML) handle side effects like printing? I'm aware of things like the IO monad in Haskell but I'm ...
thoughtpolice's user avatar
0 votes
2 answers
90 views

How do you justify making algorithm subroutines more efficient when Big-O notation only includes the dominant term?

I don't really understand time complexity, and wanted some clarification in this hypothetical situation. If I were being given items one by one, and I wanted a list of them all in the reverse order I ...
Matt's user avatar
  • 103
5 votes
1 answer
698 views

Resources for implementing dependent type theory

I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
thoughtpolice's user avatar
1 vote
2 answers
101 views

Relation between programming languages requiring declaration of variables before use and using the token class $\text{id}$ while parsing

I was going through the text Compilers: Principles, Techniques and Tools by Ullman et. al. where I came across the following excerpt. Example 4.11. Consider the abstract language $L_1 = \text{ { $wcw$...
Abhishek Ghosh's user avatar
5 votes
2 answers
941 views

Break keyword outside a loop is syntax error or semantic error?

I am designing a simple compiler for my university project. In my programming language, the break keyword is allowed. I want to know whether break keyword occurs outside a loop should be a syntax ...
Buddhika Chathuranga's user avatar
2 votes
0 answers
39 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
4 votes
1 answer
68 views

Proving equivalence of two substitutions by induction

I'm trying to prove the following reduction: $$ t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\} $$ under the following assumptions: $x \neq y$ $x$ is not a free variable of $v$ (in symbols, $x \...
user206904'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
0 votes
0 answers
153 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
20 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
4 votes
1 answer
161 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?
user56834's user avatar
  • 3,692
3 votes
3 answers
1k 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 (...
user56834's user avatar
  • 3,692
5 votes
2 answers
721 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 ...
Charlie Parker's user avatar
1 vote
1 answer
88 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 ...
kansas_bulldog382's user avatar
10 votes
1 answer
158 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 ...
helianthus's user avatar
2 votes
1 answer
68 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 ...
Charlie Parker's user avatar
2 votes
1 answer
38 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 \...
user1868607's user avatar
  • 2,194
8 votes
1 answer
258 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 ...
user1868607's user avatar
  • 2,194
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
0 votes
2 answers
136 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 ...
TomR's user avatar
  • 1,381
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
1 answer
128 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 ...
Tim's user avatar
  • 4,875
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
1 vote
1 answer
347 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?
Ahmed Abdullah's user avatar
3 votes
1 answer
43 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))=\...
ysalmon's user avatar
  • 233
1 vote
0 answers
208 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
9 votes
1 answer
9k 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 ...
George's user avatar
  • 193
2 votes
2 answers
1k 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)...
Jack's user avatar
  • 23
5 votes
0 answers
132 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
5 votes
1 answer
368 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 ...
user1868607's user avatar
  • 2,194
3 votes
1 answer
518 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 ...
user1868607's user avatar
  • 2,194
2 votes
1 answer
780 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 \...
Charlie Parker's user avatar
0 votes
1 answer
53 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 ...
user1868607's user avatar
  • 2,194
1 vote
1 answer
57 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; ...
Charlie Parker's user avatar
1 vote
2 answers
294 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, ...
Charlie Parker's user avatar
2 votes
2 answers
230 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 ...
Mathias Vorreiter Pedersen's user avatar
2 votes
1 answer
77 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 ...
Himanshu Kansal's user avatar
2 votes
1 answer
38 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 ...
deadphoenix'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
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
3 votes
1 answer
139 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 ...
Harr's user avatar
  • 31