12 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 ...
gasche's user avatar
  • 2,040
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 ...
Andrej Bauer's user avatar
  • 28.8k
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 ...
Damiano Mazza's 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 ...
ShreevatsaR's user avatar
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 ...
András Kovács's 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.
Martin Berger's user avatar
8 votes

Formal semantics of tactics

Obviously there is an operational semantics of Ltac by Jedynak et al.
xrq's user avatar
  • 1,175
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 ...
cody's user avatar
  • 13.8k
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 ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.8k
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 ...
Noam Zeilberger's 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). ...
Martin Berger's 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 ...
gasche's user avatar
  • 2,040
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 ...
Samuel Schlesinger's user avatar
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\...
Damiano Mazza's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.8k
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 ...
gasche's user avatar
  • 2,040
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 ...
Noam Zeilberger's 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 ...
cody's user avatar
  • 13.8k
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 ...
varkor's user avatar
  • 246
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 ...
varkor's user avatar
  • 246
4 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 ...
Martin Berger's 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 ...
Jay's user avatar
  • 982
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 "...
Domenico Ruoppolo's user avatar
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 ...
Jay's user avatar
  • 982
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 ...
Max New's user avatar
  • 1,675
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 ...
Evan Patterson's user avatar
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 ...
Dan Doel's user avatar
  • 931
2 votes

Are there logical devices similar to "existential variables" or "blank nodes" of Semantic Web?

I cannot answer for research in logic about blank but I can try to explain blank nodes. In my (possibly faulty) comprehension of the W3C standard, blank nodes are "existential variables" in ...
Louis's user avatar
  • 775
2 votes
Accepted

Is there an official/academic name for the "current value" in a loop?

There is no official name for a variable used in a loop because it depends on how it is used and what it is used for. For instance, it could be a state, pointer, iterator, index, counter, flag, ...
tylerh111's user avatar
  • 136

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