34
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'
38.4k7 gold badges102 silver badges166 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 ...
15
Why not to learn semantics of C right away instead of inventing
another language, for describing semantics of C?
Because in order to define the semantics of C you need some kind of language, for example English. English can be ambiguous, and especially is the C99 semantics.
The computer science notion of semantics is generally a mathematical description ...
15
Jean Louis Krivine introduced an abstract calculus which extends the "Krivine Machine" in a very non-trivial way (note that the Krivine machine already supports the call/cc instruction from lisp):
He introduces a "quote" operator in this article defined in the following manner: if $\phi$ is a $\lambda$-term, note $n_\phi$ the image of $\phi$ by some ...
12
Converge has some pretty impressive meta-programming facilities.
At a simple level, this can be seen as a macro-like facility, although it is more powerful than most existing macro facilities as arbitrary code can be run at compile-time. Using this, one can interact with the compiler, and generate code safely and easily as ITrees (a.k.a. abstract syntax ...
11
The definition of continuity used by your teacher is the nicer one. It tells you pretty concretely what continuity means.
Suppose $b \in f(x)$. That means that given all the information of $x$, possibly an infinite set of tokens (atoms), the function produces some element that has the atomic piece of information $b$. (It could have other information too, ...
11
Overloading is when two or more methods have the same name but different signature (different argument types, different number of arguments). Overloading is resolved statically, depending only on the static types of the arguments. (The interaction of overloading and overriding, in Java, for example, makes the story a little more complicated). Overloading ...
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
There are two parts of the semantics you will need to describe:
static semantics: structure of well formed programs
dynamic semantics: meaning of running programmings
Static semantics usually take the form of type systems. I'd recommend looking at the books by Benjamin C Pierce and Robert Harper. Alternatively, you could write the rules of well-formed ...
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
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 ...
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
Doing so is very difficult, if not imposible, without giving up confluence. Which is to say, I suspect you are right about a hairy meta-theory. On the other hand, it is possible to design a combinator calculus that can express all turing computable functions, and that has full ability to inspect its terms: see Jay and Give-Wilson .
I believe that having ...
8
Sounds like you are reading The Art of Multiprocessor Programming.
"All function calls have a linearization point at some instant between their invocation and their response"
Okay that's fine, they occur somewhere within a function call, but what are they?
Side effects of the functions. http://en.wikipedia.org/wiki/Side_effect_(...
8
"Is it theoretically feasible?*
Of course, it is. One can always write an interpreter in a language ($L$) for another language ($S$), and write programs in the new language. People do not often do this because it might involve a lot of work to write such an interpreter and there will be a performance hit (a factor of 10-100) for the additional layer of ...
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'
38.4k7 gold badges102 silver badges166 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
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
The input format for the tool OTT is based on ASCII and the rules look very much like type system/operational semantics rules. Maybe you could use that format. I'm sure that the parser for the input format is available as open source.
7
If you allow one function to call another, then you have enough power to distinguish a lexically defined variable from a dynamically defined one.
def scope {
var x = 10
def f() {
return g()
}
}
def g() {
return x;
}
scope.f()
If x is dynamically scoped, the code returns 10. If it is lexically defined, the result is an error.
Thus if you want ...
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 ...
Only top voted, non community-wiki answers of a minimum length are eligible
