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 ...
user avatar
  • 26.6k
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 ...
user avatar
  • 1,882
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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.
user avatar
8 votes

Formal semantics of tactics

Obviously there is an operational semantics of Ltac by Jedynak et al.
user avatar
  • 1,125
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 ...
user avatar
  • 26.6k
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 ...
user avatar
  • 13.2k
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 ...
user avatar
7 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 ...
user avatar
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). ...
user avatar
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 ...
user avatar
  • 1,882
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, ...
user avatar
  • 1,882
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 13.2k
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 ...
user avatar
  • 26.6k
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 ...
user avatar
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 ...
user avatar
  • 1,882
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 "...
user avatar
4 votes

Categorical semantics for non-monotonic logics?

Non-monotonic logic is kind of a wide area -- do you have any particular logics in mind? Anyway, defeasibly assuming :) that you are interested in any logic in which the principle of monotony fails, ...
user avatar
4 votes

What requirements should a denotational semantics for a programming language satisfy to be correct?

What I am writing is essentially contained in babou's answer. But I wanted to express it a bit differently emphasizing the point of defining formal semantics. A formal semantics is a mapping from ...
user avatar
  • 21.3k
4 votes
Accepted

What is the relation/difference between axiomatic and denotational semantics one one side, and the data flow analysis(DFA) on the other sied?

The textbook that might be most relevant to your question is Principles of Program Analysis by Nielson, Nielson and Hankin. It does cover dataflow analysis and its relationship to denotational ...
user avatar
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 ...
user avatar
  • 962
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 ...
user avatar
  • 962
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 ...
user avatar
  • 196
4 votes

"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 ...
user avatar
  • 1,412
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 ...
user avatar
3 votes

Books on programming language semantics

For a complete beginner studying operational semantics, I would suggest Programming Languages and Operational Semantics by Maribel Fernández. Everything is explained in a very simple manner which is ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible