31
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-...
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
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 ...
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 ...
12
Because a CCS process is worth a thousand pixels – and it is easy to see the underlying LTS – here are two processes that simulates each other but are not bisimilar:
$$P = ab + a$$
$$Q = ab$$
$\mathcal{R_1}=\{(ab+a, ab), (b, b), (0,b), (0, 0)\}$ is a simulation.
$\mathcal{R_2}=\{(ab, ab+a), (b, b), (0,0)\}$ is a simulation.
$P\ \mathcal R_1\ Q$ and $Q\ \...
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
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
Even if there's a simulation in each direction, the simulations back and forth may not relate the same sets of states. Sometimes you have a simulation $R_1$ in one direction, and a simulation $R_2$ in the other direction, and two states $p_1$ and $q$ which are related by $R_1$ but not by $R_2$ nor by any other simulation in the same direction.
The canonical ...
10
May I direct you to the Funarg problem wikipedia page? At least this is how the compiler people used to reference the closure implementing problem.
So a closure is essentially a (anonymous?) function value which can use variables outside of its own scope. In my experience, this means it can access variables that are in scope at its definition point.
...
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
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 ...
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
"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
Your axiom is not really an axiom, it's missing hypotheses. Simple presentations of Hoare logic manipulate formulas of the form $\{P\} C \{P'\}$ where $P$ and $P'$ are logical formulas and $C$ is a command. You do need to ensure that $C$ is well-formed. In simple languages such as the ones often used for a first introduction to Hoare logic, well-formedness ...
8
A little terminology may help if you want to look this up: these rules are rewriting rules, they have nothing to do with type systems¹. The property you're trying to prove is called confluence; more specifically, it's strong confluence: if a term can be reduced in different ways at one step, they can converge back at the next step. In general, confluence ...
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
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 ...
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
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
Okay, so let's consider the case that $r = \mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$, $s$ has been derived by applying the E-If rule and $t$ has been derived by applying the E-Funny rule: So $s = \mathtt{if}\: t'_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ where $t_1 \rightarrow t'_1$ and $t = \mathtt{if}\: t_1 \:\mathtt{then}\...
Only top voted, non community-wiki answers of a minimum length are eligible
