# Tag Info

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 ...
• 26.6k

### 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 ...
• 1,882
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 ...
• 4,823
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

### 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 ...
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.
• 10.3k

### Formal semantics of tactics

Obviously there is an operational semantics of Ltac by Jedynak et al.
• 1,125

### 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 ...
• 26.6k
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.2k
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 ...
• 31.6k
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,349

### 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). ...
• 10.3k
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 ...
• 1,882

### 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, ...
• 1,882

### 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,552

### 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,319
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.2k
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 ...
• 26.6k

### 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,319

### 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 ...
• 1,882

### 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 "...

### 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, ...
• 31.6k

### 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 ...
• 21.3k
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 ...
• 10.3k

### 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 ...
• 962

### 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 ...
• 962

### 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 ...
• 196

### "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,412