13

Comparing two programming languages is difficult is a difficult problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is compelling. The most widely used approach, coming from logic, is to consider translations between the languages to be compared. The general idea is as ...


12

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of fullness. But, there is also some vague connection between them. So, this is going to be a complicated answer. Full completeness: "Sound and complete" is a ...


11

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 entities, i.e., finite configurations without any a priori meaning. A language is described by the grammar, which determines which finite configurations are valid ...


11

A semantics of a program is a model of its behavior which, like any scientific model, ignores aspects that you don't want to study. An extremely detailed model of the execution of a program would model the physical behavior of the computer that executes it, including the execution time, power consumption, electromagnetic radiation, etc. Such aspects are ...


11

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 idea, and your motivation of using it to perform optimizations sounds reasonable -- another related question is whether you could define a bytecode format for it ...


10

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove that the program is equivalent to the original, stop; otherwise keep searching. This algorithm is sound. In order for it to be complete, you need to be able to ...


10

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 good thing to have a 0 around in our set of natural numbers). One possible technical exemplification of this (but there are probably dozens more, perhaps more ...


9

(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 typesetting, not for programming; so it is at best “weird” when considered as a programming language. — Donald Knuth, Digital Typography, page 235 I have read a ...


8

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 the order in which a language evaluates its arguments. A parameter-passing strategy is what the language hands to the function. To understand the connection ...


8

Obviously there is an operational semantics of Ltac by Jedynak et al.


8

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.


7

I essentially agree with Martin's comment, I can elaborate on that to make a tentative answer, knowing that there is no general formal definition of calculus or abstract machine and that what I am going to describe cannot possibly cover the meaning of all instances of these two words found in the literature. In brief: a calculus usually gives you the ...


7

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 being very, very low. John Reynolds' book Theories of Programming Languages has one of the more comprehensive explanations in its chapter 1, as does Robert ...


7

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 automaton required to recognize that language, with, e.g. Context-free languages only requiring pushdown automata (PDA) General recursive languages requiring ...


7

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 non-termination, but then we disallow handling it, as that would allow us to implement the Halting oracle. Such treatment of non-termination is a bit naive. A ...


6

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). Increasingly formal semantics is also used in automatic and interactive program verification, which is beginning to see industrial use. Since you are interested ...


6

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 seen spawn from these ideas is to understand the execution of a logic program as proof search in simple and expressive logics, such as intuitionistic logic or ...


6

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, in the sense that I suspect relatively few people of the field will spontaneously give this answer if you ask them "would you distinguish the names 'reduction ...


6

You should get acquainted with inductive definitions. Instead of saying that $Data$ is recursively defined, say that it is a set constructed inductively by: $(0,i) \in Data$ for every $i \in \mathbb{Z}$, $(1,d) \in Data$ for every $d \in Data$, $(2,d) \in Data$ for every $d \in Data$. Another way to say the same thing is that $Data$ is the smallest set ...


6

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 a fixed point under beta reduction to define the total reduction, as long as you have the nice normalization properties.


6

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 Kozic, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc. Asymptotically almost all λ-terms are strongly normalizing. Logical Methods in Computer Science,...


5

Summary: full completeness means that the interpretation function is not just complete, but also surjective on programs. Full abstraction has no requirement for surjectivity. $\newcommand{\semb}[1]{[\![ #1 ]\!]}$ Details: The detailed meaning of full abstraction and full completeness depends on the nature of what/where/how you are interpreting. Here is a ...


5

There are unfortunate confusions in the way you have posed the question. Programs have semantics. Programming Languages are given semantic definitions. In more detail: every program has a meaning, either as a computation or as a mathematical function (relation, trace set, strategy,...). A semantic definition is given for an entire programming language, ...


5

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 free algebra $A$ for the theory of $E$-exceptions, with generators from $X$. The algebra $A$ contains everything that we can generate from the generators and ...


5

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 first appears, at least in classical rewrite theory because it behaves poorly under substitution: If $t\rightarrow t'$ is an inevitable reduction, and $t$ ...


5

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 in the past, and they have much to gain from further interaction. Two classical examples of this (respectively from the 1950s and '70s) are Lambek grammar and ...


5

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 rewrite rules $$p~(S~t) \to t \qquad p~0 \to 0$$ with $$\mathsf{size}(0) = 1 \qquad \mathsf{size}(S~t) = 1 + \mathsf{size}(t) \qquad \mathsf{size}(p~t) = 1 + \...


4

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 semantics. It does not deal with axiomatic semantics though.


4

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 generated by single different symbols, when you write down the grammar. So a syntactic domain is a subset of your language, and each domain is generated by one ...


4

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 Stump's book is concise but very clear.


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