11
votes
Accepted
Standard reference for basic model theory definitions
Here is one possibility, but other people might use different words. I will use first-order logic as a running example.
Language
The language is a collection of expressions, which are syntactic ...
- 28.1k
11
votes
Has the semantics of TeX (as a programming language) ever been formalized?
No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in.
(What follows is a subjective and personal commentary). I think it is an intriguing and well-posed ...
- 2,030
10
votes
Accepted
Why is the multi-step reduction of semantics reflexive?
The practical reason is that it is very convenient to include also the case "zero steps" in the definition of "many steps" (millennia of mathematical experience have taught us that it is usually a ...
- 5,253
9
votes
Accepted
Has the semantics of TeX (as a programming language) ever been formalized?
(With apologies for a long answer that goes in a direction different from the scope of the site: frankly I was surprised to see the question here in the first place….)
TeX was designed for ...
- 295
8
votes
What's the difference between reduction strategies and evaluation strategies?
A reduction strategy is a function on Lambda that picks one redex (reducible expression) from all possible redexes -- depending on what you define as a redex.
Informally, an evaluation strategy is ...
8
votes
Accepted
Formal semantics of tactics
I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.
- 11.3k
8
votes
Formal semantics of tactics
Obviously there is an operational semantics of Ltac by Jedynak et al.
- 1,155
8
votes
Accepted
What's the categorical semantics of definitional equality?
Definitional equality is the same as equality in the metatheory. It works exactly the same way as in 1-category theory. If I have a category $\mathbb{C}$ and some morphisms $f,g : \mathbb{C}(A, B)$, I ...
- 1,444
7
votes
Can Non-termination be considered an algebraic effect?
Non-termination can be considered an algebraic effect up to a point. It's an exception that cannot be handled. More precisely, we may introduce a nullary operation (constant) $\bot$ which signifies ...
- 28.1k
7
votes
Accepted
Difference between syntax and semantic error in programming languages
In the strictest sense, there is no real difference between syntax errors and semantics errors, at least as far as language theory is concerned: the only salient difference is the complexity of the ...
- 13.7k
7
votes
Accepted
Precise definition of syntatic categories / syntatic domains in abstract syntax
Most people avoid giving precise descriptions of what a syntactic category is, because if you do it properly with all the details, the ratio of insight to necessary mathematical sophistication ends up ...
- 32.3k
6
votes
What's the difference between reduction strategies and evaluation strategies?
The "Reduction strategy" wikipedia article is entirely extracted out of a particular edit made by an anonymous IP to the "Evaluation strategy" article.
The view that it represents is not consensual, ...
- 2,030
6
votes
In what fields does a knowledge of formal semantics prove useful?
Formal semantics is useful primarily when you want to reason about programs.
In the past this was mainly done in programming language development (and to a lesser degree in compiler construction). ...
- 11.3k
6
votes
Accepted
How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses
You should have a look at Uniform Proofs as a Foudation for Logic Programming by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has ...
- 2,030
6
votes
Why is the multi-step reduction of semantics reflexive?
The answer given is adequate but I'd like to mention that once you reduce a term to normal form, without reflexivity you're out of luck, with reflexivity you've hit a fixed point and thus you can use ...
- 1,562
6
votes
Density of semantics in syntax
In terms of related work, Marek Zaionc and collaborators have been studying similar kinds of questions for some time. The following paper includes many results:
René David, Katarzyna Grygiel, Jakub ...
- 4,411
6
votes
Accepted
Terminal object in the category of embeddings
The answer is no.
Let me first rewrite the definition given in the comments: an arrow $f:D\to E$ of $\mathbf{CPO}$ is an embedding if there exists $g:E\to D$ such that $g\circ f=\mathrm{id}_D$ and $f\...
- 5,253
5
votes
Density of semantics in syntax
Let's look at a simple example of a toy programming language with unary natural numbers and a "predecessor" operation.
$$t ::= 0 \mid S~t \mid p~t$$
whose semantics is given by the following ...
- 2,030
5
votes
What relations and differences are between formal semantics for linguistics and for programming languages?
This question is very open-ended and therefore difficult to answer, but I think the short answer is "yes", there is much common ground, the two areas have in fact benefited from interaction ...
- 4,411
5
votes
Accepted
Is there a notion of "inevitable reduction?"
I have never heard of this exact concept in rewrite theory, which certainly doesn't prove it hasn't been considered.
However, I will make the point that it may not be quite as useful a concept as it ...
- 13.7k
5
votes
Accepted
What is a 'free model'?
Consider a set $E$. The theory of $E$-exceptions is an algebraic theory given by:
for every $e \in E$ a nullary operation symbol $\mathsf{raise}_e$
no equations.
Given a set $X$, we may consider the ...
- 28.1k
5
votes
Does ${\bf CPO}$ have $\omega$-colimits?
If you relax the assumption that the CPOs have bottom elements (i.e. initial objects), or require that the morphisms also preserve the bottom element, then the answer is yes.
CPOs (respectively CPOs ...
- 246
4
votes
Precise definition of syntatic categories / syntatic domains in abstract syntax
I never found an explicit definition either, but I have inferred the folowing.
As I understand, you split the language into syntactic domains; with the addition that syntactic domains must be fully ...
- 972
4
votes
Categorical semantics for non-monotonic logics?
[My apologies for writing this as an answer, despite the fact that it is basically just a comment to the previous answer. But I am not allowed to post a comment up there, since I do not have enough "...
4
votes
Books on programming language semantics
I would like to add two books not found on the answers given up to now:
Aaron Stump, Programming Language Foundations
David Schmidt, Denotational Semantics: A Methodology for Language Development
...
- 972
4
votes
What's the categorical semantics of definitional equality?
Definitional equality is essentially a syntactic notion of equality, not witnessed by a term in the type theory: when two types or terms are definitionally equal, we are saying that they are precisely ...
- 246
4
votes
Accepted
"Operations" in category theory that are not defined for arrows
There are several ways to formalize this idea in category theory that I have seen in the literature.
An overview is that you can either separate the two occurrences of $D$ into the positive and ...
- 1,638
3
votes
Can Non-termination be considered an algebraic effect?
You may be interested in this paper. It describes things in terms of monads, but the idea is that you define an 'effect' of making a recursive call. Then appropriately typed functions can be ...
- 911
3
votes
Accepted
What does the category of RDF models look like in Institution Theory?
There's a lot to unpack here and I don't know about Goguen's institutions. But perhaps I can give a partial answer to your question.
Let's start with "simple interpretations" of RDF, as defined by ...
3
votes
Accepted
Semantics of logic/relational programming languages
A good place to start might be Datalog which has various clean approaches to semantics. A Datalog program is (simplifying a bit) a function-free and negation-free Prolog program.
For the semantics of ...
- 11.3k
Only top scored, non community-wiki answers of a minimum length are eligible