Skip to main content
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
  • 29.2k
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,185
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
  • 29.2k
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.9k
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
6 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
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

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
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.9k
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
  • 29.2k
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

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
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
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,695
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

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
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
  • 1,021
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
2 votes

Difference between syntax and semantic error in programming languages

It is hard to say. The boundary between "syntactic errors" and "static semantic errors" can be really blurred. One appropriate example would be Curry-style (extrinsic typing) and Church-style (...
xrq's user avatar
  • 1,185
2 votes

Observational Equivalence of open terms in PCF

Got the answer, thanks to jonsterling on reddit for the insight. The error is that both M and N written as full judgements, ...
Adribar's user avatar
  • 31
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
2 votes

Semantic read-back of sharing graphs

I do not have a proper answer, but you might want to have a look at this paper by Asperti where there is a study of sharing graphs inspired by category theory.
Beniamino Accattoli's user avatar
2 votes

Can Non-termination be considered an algebraic effect?

In 2004 D. A. Turner argued in an easy to read article Total Functional Programming that non termination is a problem with interpreting languages like Haskell purely mathematically, but that to ...
Henry Story's user avatar
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

Operational semantics and denotational semantics and describing the behaviour and structure of programs

I am going to attempt an answer, or more precisely a clarification, but one should keep in mind that most ingredients of the question (semantics, operational, behavior, structure) do not have a clear ...
Beniamino Accattoli's user avatar

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