37
Small-step semantics defines a method to evaluate expressions one computation step at a time. Formally speaking, a small-step semantics for an expression language $E$ is a relation $\rightarrow : E \times E$ called the reduction relation. Small-step semantics describes what happens to an expression in detail. It's able to give a precise account of even non-...
answered Jun 7 '15 at 2:13
Gilles 'SO- stop being evil'
39.9k7 gold badges106 silver badges171 bronze badges
25
This is a standard notation for an inference rule. The premises are put above a horizontal line, and the conclusion is put below the line. Thus, it ends up looking like a "fraction", but with one or more logical propositions above the line and a single proposition below the line. If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's ...
11
There is no real agreement what characterises denotational semantics (see also this article), except that it must be compositional. That means that if $\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack} \SEMB{\cdot}$ is the semantic function, mapping programs to their meaning, something like the following must be the case for all $n$-ary program ...
10
Note: parameter passing by xxx is sometimes called "pass by xxx" and
sometimes "call by xxx". I will use both expressions indifferently.
Parameter passing by value-result consists in passing by value when the
subprogram (whatever it is) is called, and then, when it terminates,
assign the current value of the formal parameter in the subprogram
back to the ...
10
It's the greatest fixed point, or the final coalgebra, depending on how you set things up. In Haskell it is impossible to define the datatype of finite lists because Haskell does not have inductive types, only the coinductive ones. Many people are in denial about this particular issue.
10
The meaning of the words is not fixed, but I can give you my interpretation.
A calculus is something that we calculate with in the sense of juggling equations (think manipulation of Taylor series or computation of integrals in analysis). A calculus tells us what the rules of manipulation are, but not which ones we should used in a given situation.
A ...
9
Swift guarantees that once the last reference to an object is dropped the object is deinitialized, and the deinit code is immediately run.
Obtaining this kind of guarantee through GC is not possible - at least, not without sacrifying performance. Standard GC mechanisms only ensure the deinit code is eventually run, e.g. at the next GC cycle. For precise ...
9
There are many compilers, which compile widely different kinds of languages which serve widely different purposes. For example, a database language will have very different optimizations than an array-based language like APL.
Compilers themselves use several intermediate languages, from the input language, to a de-sugared version of the input language, all ...
8
The subtlety lies in where the distinction between language and metalanguage is made. As René Magritte put it:
$(\lambda f. \lambda x. f x) ((\lambda y.y) (\lambda z.z)) (\lambda w.w)$ is a lambda-term, written in the syntax for lambda-terms. Let's call this lambda-term $t$. Let $M$ be the lambda-term $(\lambda f. \lambda x. f x) ((\lambda y.y) (\lambda ...
answered Apr 1 '14 at 7:08
Gilles 'SO- stop being evil'
39.9k7 gold badges106 silver badges171 bronze badges
8
Semantics of a logic describe how to compute the truth value of an expression, possibly given some interpretation. For example, one rule would say that an expression $\varphi \land \psi$ is true iff both $\varphi$ and $\psi$ are true, and another would say that $\forall x \varphi(x)$ is true if for all $x$ in the domain of discourse $D$ (which forms part of ...
8
First of all, note that the notion of a formal system is an informal notion and there is no general (or generally accepted), formal definition of what a formal system is. In my opinion, the Wikipedia article on formal systems does not do a good job at explaining this and creates the illusion that formal systems are more or less the same as (the syntactic ...
8
To answer this question, it's best to reflect on the meaning of sums in process calculi. Essentially sums express a lack of knowledge. The process $P + Q$ means something along the lines of "either $P$ or $Q$ is active, but I have absolutely no information which". Note that this is related to, but different from a probabilistic sum like
$P +_{0.5} Q$ which ...
8
The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition.
For example, given a program sqrt with the postcondition that sqrt(x) = y and y*y = x, what are some valid preconditions?
x > 10
x > 20
x > 1
Some invalid preconditions would be
x < 0
x > -10
One predicate P1 is ...
8
What you call "equational dynamics" is not actually an operational semantics, it's an equational theory. As you note, equations by themselves do not tell us how to run programs. However, they are needed because we want to express the idea of program equivalence. For instance, an optimizer replaces a piece of code with an equivalent piece of code (which is ...
8
Although there are frameworks created specifically for the purpose of prototyping programming languages (including their semantics, type systems, evaluation, as well as checking properties about them), the best choice depends on your particular case and specific needs.
Having that said, there are multiple (perhaps not so distinct) alternatives you might ...
8
Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, then $B$ is weaker than $A$. Note that, from the definition, $A$ is stronger and weaker than itself, since $A$ implies $A$. (We might prefer to ...
8
There is an (operational) semantics for Java 1.4 formulated in the $\mathbb{K}$ framework. Associated to this framework is a proof system called Matching Logic. While that page describes a prototype implementation, it seems that the functionality is being incorporated into the $\mathbb{K}$ framework tools themselves as kprover. Unfortunately, it seems the ...
7
Unfortunately there aren't many textbooks on the topic. I think the best way to learn program analysis today is to survey different courses that are available, play with a few implementations and then look at a few research papers for your specific needs. What follows is a very small sampling of what's out there. Since you specifically mentioned compiler-...
7
The answer to your literal question, "Does a logical system have semantics?" is "Obviously, yes. The definition you quoted says so!" So I figure that isn't what you're actually asking.
I think the root of your misunderstanding is the word "formal". In this context, it doesn't mean "rigorous", the opposite of "hand-wavy"; it means "depending on form". That ...
7
Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition!
The Ap is the state of your system or your running program. "State" can mean a lot of things but in this case it seems to include a list of all defined local variables and their values. Why is Ap a ...
7
Featherweight Java is quite highly regarded in the PL community. But if that doesn't suit your needs, here's a general approach to modelling:
Formalize your language's AST into expressions and statements
Write a semantics for expressions and statements. Your semantics will need:
an evaluation relation, relating expression-state pairs $(e,\sigma)$ to an ...
7
Although I personally would describe type analysis as semantic, this question seems to start with the assumption that there is a clear, formally-definable dividing line between "syntax" and "semantics".
I don't think that is the case; even if most of us would put type-correctness into one category and missing parentheses into the other one, there is a ...
6
Devising an operational semantics of a programming language requires ingenuity, just like engineering a new car does. Nevertheless, there are some principle and correctness criteria by which we can judge whether a given semantics is "good".
For example, a good operational semantics should make sure that "valid programs do not do bad things". In practice ...
6
Can you come up with two different algebras, say, one where the domain is $\mathbb{N}$ and one where the domain is $\{0,1\}$ and in the former, suc and pred work as you would assume, and in the latter, they are modulo 2 operations? Then, try to come up with a homomorphism from one to another.
Then, try to make an algebra, where the domain is $\{0, s0, ss0, ...
6
The language of inference rules are much more general than what is usually given in Logic. Indeed you can look at systems with rules of the shape
$$ \frac{\Theta_1\ldots \Theta_n}{\Theta}$$
Where the $\Theta_i, \Theta$ are some kind of statement and ask: what are all the possible $\Theta$ I can get by repeated application of these rules?
In the above case,...
6
I am afraid the phrasing of the question misled me (though I did know
better) in first seeing model theory as applying to any two arbitrary
mathematical structures, and being the study of homomorphisms of
mathematical structures.
Actually this is wrong. Model Theory already contains the idea of
syntax and semantics, more or less as I define it below. It ...
6
Your proposed alternate definition is no good. It tries to define $[[\text{while b do S}]]$ in terms of $[[\text{while b do S}]]$. That's a circular definition: you can't define something in terms of itself.
"FIX" typically refers to the least fixpoint, and is a way of avoiding circularity. See your textbook for background on fixpoints and the precise ...
6
In general matching with dependent types can be quite subtle! You'll note that in the Coq documentation that the extended pattern-matching syntax is
match t as x in T1 return T2 with
| C1 a1 ... an
...
In particular, ommiting any of the as, in or return clauses can prevent type inference of the statement.
Intuitively, if the type of (say) ...
6
I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type $\sigma + \tau$ for any $\tau$. The names of type variables don't matter, what matters is where else are you using the same type variable.
6
Are extensions required? Not really. You can take an axiomatic description of a modal logic and simply provide a "primitive" lambda term for each. The modal operators would become type constructors. Haskell's IO monad can be viewed this way. Coherence conditions like the monad laws would provide some conversions between terms.
A different approach, which ...
Only top voted, non community-wiki answers of a minimum length are eligible
