18

"Meaning" is used in a broader way than denotation is. The original dichotomy, inherited from logic and philosophy, is between "sense" and "denotation" (which philosophers call "reference"). This distinction can be illustrated by Frege's original example. He noted that phrases "the morning star" and "the evening star" referred to the same object --- the ...


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

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

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

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

Landin's SECD machine, originally described in The mechanical evaluation of expressions in 1964, is a transition system in the form of an abstract machine, later inspiring lots of of other abstract machines such as the CESK machine.


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

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

I don't know how you can define the informal semantics as accurately as possibly, but there does exist machinery for defining semantics that is purely, well, semantic. Your semantics could be based on mathematical functions, relations, or domains. Indeed, the style of semantics known as Denotational Semantics builds upon these (and other) semantic notions ...


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

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

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.


5

Legally speaking, the term "calculus" is almost always used to describe a language, i.e., a piece of syntax, with added rules of calculation or reasoning. Examples include the good old predicate calculus, lambda calculus, process calculi, various type theories and logics (e.g., Martin-Lof type theory and linear logic). From a programming language point of ...


5

There's Amir Pnueli's 1977 The Temporal Logic of Programs, where (as you doubtless know) the transition system is viewed as a Kripke frame. He cited the Keller paper you mention as his source of the idea that programs are transition systems. (I've never seen that one though.) Christopher Strachey gave semantics to stateful programs as state transformers on ...


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

this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification. some of this technology is apparently utilized in the CompCert C compiler. A structured approach to proving compiler optimizations based on dataflow analysis it considers the correctness of two ...


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

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


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$ ...


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