Questions tagged [semantics]
Semantics formally describe the meaning of some syntax.
179
questions
2
votes
1
answer
65
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 ...
- 30.4k
0
votes
1
answer
34
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:
...
- 30k
0
votes
1
answer
63
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?
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} \...
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 ...
- 111
5
votes
2
answers
5k
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 ...
- 3
41
votes
2
answers
13k
views
Difference Between Small and Big-step Operational Semantics
What's the fundamental difference(s) between small and big-step operational semantics?
I'm having a hard time grasping what it is and the motivation for having the two.
- 111
0
votes
1
answer
54
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$ ...
- 3
5
votes
2
answers
3k
views
Static scope and dynamic scope
I am perpetually confused when it comes to static scoping and dynamic scoping and their differences and Wikipedia isn't of any help, so here's my question:
Given the following pseudo code in a ...
8
votes
1
answer
2k
views
Lambda Calculus: How do evaluation contexts "work"
In the pure lambda calculus, we have the inductively defined set of terms (the grammar):
$$e::= x \mid \lambda x . e \mid e_1 e_2$$
Under the call-by-value evaluation strategy, we have the inference ...
- 103
13
votes
4
answers
1k
views
Getting started with Program Analysis
I'm looking for resources on getting started with program analysis.
The only book I've found on the topic is the Nielson & Nielson book.
Other than that, it seems like there are only "compiler" ...
- 101
2
votes
1
answer
624
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 ...
- 30.4k
5
votes
1
answer
243
views
Notation for operational semantics that can be used in code comments
I'm defining an intermediate language for a multi-backend code generator that I'm writing. I want to document the operational semantics for this intermediate language in a way that is readable both ...
- 5,101
5
votes
1
answer
377
views
Why injection into sum type apparently leads to ambiguity?
I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that ...
- 5,101
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 \...
- 5,101
4
votes
2
answers
458
views
How does one deduce small step operational semantics?
This question arises from my reading of "Types and Programming Languages" (WoldCat) by Benjamin C. Pierce.
For the small step operational semantic evaluation rules for the arithmetic expressions (NB) ...
- 5,101
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 ...
- 5,101
8
votes
1
answer
259
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 ...
- 5,101
3
votes
1
answer
289
views
Proof via induction for small-step semantics
I'm doing a course in Computer Programming Languages and I'm trying to prove the following (roughly following Pierce's Types and Programming Languages book):
if $t \rightarrow^* t'$ then $if\; t\; ...
- 8,248
1
vote
1
answer
83
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 ...
CommunityBot
- 1
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)...
- 1
3
votes
2
answers
130
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 ...
- 30.4k
0
votes
2
answers
91
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 ...
- 1,910
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))=\...
- 233
5
votes
1
answer
733
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? ...
- 29.8k
1
vote
2
answers
103
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$...
- 6,140
5
votes
2
answers
944
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 ...
- 30k
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 ...
- 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 \...
- 277k
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 (...
- 22.1k
3
votes
0
answers
92
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 ...
- 370
10
votes
1
answer
162
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 ...
- 3,075
0
votes
0
answers
156
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?
- 65
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;
...
- 661
2
votes
1
answer
71
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 ...
CommunityBot
- 1
5
votes
2
answers
739
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 ...
- 3,040
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 ...
- 379
4
votes
1
answer
165
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?
- 659
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 ...
- 3,276
4
votes
4
answers
11k
views
Can we create recursive functions only by using if-else statements?
I have to show whether a program containing only if-else statements but no loops is able to calculate the following type of functions: $f^n(x)$. The function $f$ is applied $n$ times to $x$, so I ...
CommunityBot
- 1
0
votes
2
answers
140
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 ...
- 727
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 ...
- 121
0
votes
1
answer
54
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 ...
- 8,248
0
votes
0
answers
136
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 ...
- 1,401
3
votes
1
answer
529
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 ...
CommunityBot
- 1
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 ...
- 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 ...
- 51
1
vote
1
answer
361
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?
- 81.7k
1
vote
0
answers
211
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 ...
- 11
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 ...
D.W.♦
- 159k