Intuitionistic Propositional Logic and Natural Deduction

Here is a primer on intuitionistic propositional logic and natural deduction, along with a brief account of their historical context. The bits of historical context may explain why formal logic is somewhat entangled with the discourse on "foundations of mathematics". I frankly wanted to research and type up my notes on something else, but then started "writing backwards" and thought I'd make this the introductory notes I wish I had before learning about these things.

The topics here can be seen as useful background knowledge for anyone learning about sequent calculus, proof theory, Martin-Löf type theory (aka intuitionistic type theory aka constructive type theory), the Curry-Howard-Lambek correspondence with category theory and particularly cartesian closed categories, categorical logic; I may write about these connections at another time, but this is supposed to be an accessible overview. We proceed according to this plan:

• The beginnings of formal logic - a few words on Frege, Russell
• Axiomatic proof systems - a few words on Hilbert systems, with modus ponens as only inference rule
• What is intuitionistic logic? - a few words on Brouwer, Heyting, Kolmogorov
• Gentzen's natural deduction and sequent calculus - Gentzen creates the field of structural proof theory
• Intuitionistic natural deduction NJ - a presentation of natural deduction NJ calculus for intuitionistic propositional logic
• Natural deduction in sequent calculus style an alternative presentation that groups assumptions into "judgments" $\Gamma \vdash A$

The focus on propositional logic is for simplicity, and to build a bridge to my last post where I briefly described the Curry-Howard correspondence. One can add symbols and rules for quantifiers to obtain first-order predicate logic, and the inclined reader should consult the more detailed texts on these topics, but proof terms would no longer be simply-typed $\lambda$-calculus, and then with higher-order logic there is also a different way to talk about sets of individual objects.

The beginnings of formal logic

For ages, mathematics involved theorems and proofs. Yet, the beginning of formal logic is marked by Gottlob Frege's and Bertrand Russell's works.

Gottlob Frege described a graphical notation that captured sound reasoning in precise rules. It was the beginning of the logicist program of demonstrating that all mathematics could be carried out in formal logic. Bertrand Russell advanced this program considerably, also inventing type theory in the process.

Formal logic, symbolic logic refers to logical statements and reasoning being expressed in a formal language, with symbols representing logical statements and rules of symbol manipulation describing how to obtain new statements from existing ones, preserving validity. Frege and Russell's deductive systems of reasoning are today presented as Hilbert systems (more on those below).

Georg Cantor had proposed set theory as a foundational system earlier, but a formal account of set theory had to wait until Zermelo published his axioms. People (including Cantor himself) had found paradoxes in set theory or what they understood to be set theory. The search for the "right" foundations continued, while alternative systems of formal logic were proposed (for example, Schönfinkel's combinatory logic, which does not use any variables). The period that followed the beginnings saw what is today called the foundational crisis of mathematics.

Axiomatic proof systems

David Hilbert and his school systematized mathematical logic, the application of formal logic to formalizing mathematics, and "metamathematics".

Around 1920, the “Hilbert style” axiomatic approach, as it is often called, was known to everyone and dominated the logical scene [1]

Hilbert systems are a uniform presentation of formal deductive reasoning and can be treated as synonymous with axiomatic proof systems. There are "logical axioms" that capture the process of sound reasoning and there are "mathematical axioms" which would capture the mathematical theory we want to formalize. The only inference rules are the rule of substitution and modus ponens. A proof is a sequence of formulas, with each term being either an axiom or derived from a previous terms by application of the inference rules. If formula $A$ is derivable this way this is written $\vdash A$.

Later, John von Neumann refined axiomatic proof systems using axiom schemes: axioms schemes contain metavariables, and all instance count as axioms and modus ponens becomes the only rule. Here is such a Hilbert-style axiomatic proof system for propositional logic, due to Jan Łukasiewicz: $$ \begin{array}{l} 1.~ A \rightarrow (B \rightarrow A) \\ 2.~ (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) \\ 3.~ (\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B) \\ \end{array} $$

The rule of Modus Ponens lets us infer from $A \rightarrow B$ and $A$ the new formula $B$. Note that the other operators $\vee$ and $\wedge$ are considered as abbrevations; this is referred to as Ockham's razor, since it uses a minimum of primitives $A \vee B$ is turned into $\neg A \rightarrow B$, and $A \wedge B$ is $\neg (A \rightarrow \neg B)$.

It is amazing that this axiomatic proof systems is complete: all tautologies can be proven from a few axiom schemes. Many texts on formal logic still use axiomatic proof system, presumably because these permit to talk about formal logic with a minimal amount of machinery for syntax and logical axioms; appealing to the deduction theorem and admissible rules hide much of the structure of the proof, which is not considered interesting to begin with; all that matters is the fact that something can be proven.

[1] Stanford Encyclopedia of Philosophy The Development of Proof Theory

[2] Stanford Encyclopedia of Philosophy The Emergence of First-Order Logic

What is intuitionistic logic?

L.E.J. Brouwer rejected the idea that logics would be prior to mathematics and proposed intuitionism as philosophy of mathematics; he understood mathematics as mental constructions that come first, before any rendering in logic.

We summarize the intuitionist positions as follows:

• An intuitionist rejects the law of the excluded middle $A \vee \neg A$ when $A$ is a statement about infinite sets
• An intuitionist rejects the idea of an "actual infinite" altogether and regards infinity as "potential infinity", approximable by repeating a process, but never completed.
• An intuitionist aims to base all mathematics on effective constructions that can be verified based on intuition (such as the intuition of being able to carry out a countable number of steps)

These restrictions avoid paradoxes of naive set theory, at the cost of rejecting large parts of established mathematical practice.

Brouwer's student Heyting [3] and also Kolmogorov [4] formulated axioms of intuitionistic logic as axiomatic proof systems.

Their efforts is what enabled further discussion (beyond philosophical disagreement) and defined intuitionistic logic [5]. Today, maybe due to the multiple available proof systems for formal logic, many sources define intuitionistic logic informally by reproducing the "Brouwer-Heyting-Kolmogorov (BHK) interpretation" [wikipedia]. This is a description of what is an acceptable proof. We skip a discussion of these because we will be giving natural deduction rules below. The key part is that structure of the proof matters now; the structure contains the constructions that the intuitionist cares about.

Intuitionistic logic is only considered one form of constructive logic and constructive mathematics; there are other logics that are compatible with the BHK interpretation, and multiple possible interpretations of the word construction and function, and then I think most mathematicians do not bother to formal logic (while still caring about precise language and rigour). A different system of logic that is motivated by enabling constructive reasoning is Martin-Löf type theory (also called intuitionistic type theory or constructive type theory).

[3] Arend Heyting (1930). Die formalen Regeln der intuitionistischen Logik., 3 Teile, In: Sitzungsberichte der preußischen Akademie der Wissenschaften. phys.-math. Klasse, 1930, 42–56, 57–71, 158–169.

[4] Thierry Coquand. Kolmogorov's contribution to intuitionistic logic. 10.1007/978-3-540-36351-4_2.

[5] Stanford Encyclopedia of Philosophy The Development of Intuitionistic Logic.

Gentzen's natural deduction and sequent calculus

Gerhard Gentzen was David Hilbert's student and sparked the entire field of structural proof theory with his seminal article and thesis that introduced both natural deduction and sequent calculus - in both intuitionistic and classical variants [6].

Gentzen was not the first to invent natural deduction. Jan Łukasiewicz observed that the axiomatic systems of Frege, Russell and Hilbert do not reflect mathematical practice; mathematicians start their proofs from assumptions, applying "proof figures" to derive new results. His student Stanisław Jaśkowski came up with a calculus of natural deduction, where derivations from assumptions are drawn in boxes [7].

Gentzen pointed out that proofs come with structure: a proof may contain a "detour", and such detours can always be removed, yielding a normal form. In order to demonstrate this, he reformulated natural deduction as the sequent calculus and the normalization through his celebrated cut-elimination theorem. In the sequent calculus, lists of formulae are manipulated (the word sequent is a random word chosen by Kleene to resemble "Sequenz"). Much later, Dag Prawitz proved the corresponding normalization result directly for natural deduction [8].

Natural deduction captures formally and precisely reflect how a mathematician proves things while still admitting a "natural" understanding of what is going on - unlike axiomatic proof systems where structure is artificial and ultimately does not matter as it was obtained by modus ponens and axioms.

[6] Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift. 39 (2): 176–210. doi:10.1007/BF01201353. (link)

[7] Stanisław Jaśkowski (1934) On the Rules of Suppositions in Formal Logic Studia Logica 1, pp. 5–32 (reprinted in: Storrs McCall (ed.), Polish Logic 1920-1939, Oxford University Press, 1967 pp. 232–258)

[8] Dag Prawitz (1965). "Natural Deduction : A proof theoretical study" (reissued 2006 Dover) \(\newcommand{\andintro}[0]{\color{blue}{(\wedge{\mathrm{\small INTRO}})}}\) \(\newcommand{\andelim}[0]{\color{blue}{(\wedge{\mathrm{\small ELIM}})}}\) \(\newcommand{\andelimleft}[0]{\color{blue}{(\wedge{\mathrm{\small ELIM/1}})}}\) \(\newcommand{\andelimright}[0]{\color{blue}{(\wedge{\mathrm{\small ELIM/2}})}}\) \(\newcommand{\orintro}[0]{\color{blue}{(\vee{\mathrm{\small INTRO}})}}\) \(\newcommand{\orelim}[0]{\color{blue}{(\vee{\mathrm{\small ELIM}})}}\) \(\newcommand{\implintro}[0]{\color{blue}{(\rightarrow{\mathrm{\small INTRO}})}}\) \(\newcommand{\implelim}[0]{\color{blue}{(\rightarrow{\mathrm{\small ELIM}})}}\) \(\newcommand{\notelim}[0]{\color{blue}{(\neg{\mathrm{\small ELIM}})}}\) \(\newcommand{\botelim}[0]{\color{blue}{(\bot{\mathrm{\small ELIM}})}}\)

Intuitionistic natural deduction NJ

We now look at the calculus Gentzen calls NJ, but for propositional logic. For notation, we use $\wedge$ instead of & for conjunction and $\rightarrow$ instead of $\supset$ for implication. Our formulae are defined as:

• $\bot$ is a formula ('falsehood')
• a propositional variable $p$ is a formula,
• if $A$ is a formula, so is $\neg A$
• if $A, B$ are formulae, so are $A \vee B$, $A \wedge B$ and $A \rightarrow B$.

We shall need to use inference rules and derivations. An inference rule has the form: $$ \frac{X_1 \quad \ldots \quad X_n}{Y} $$

with the meaning that $X_i$ are premises and $Y$ the conclusion of the rule. In natural deduction, each premise and each conclusion of an inference rules is simply a formula. A derivation is an arrangement of inference rules in tree form; the derived formula is at the bottom and inference rules connect each conclusion to premises above the bar. The derivations built up from (instance of) inference rules this way gives a proof of the formula at the root.

The rules are as follows (the notation will be explained below): $$ \cfrac{A\quad B}{A \wedge B}~\color{blue}{(\wedge\mathrm{\small INTRO})} \quad \cfrac{A \wedge B}{A}~\color{blue}{(\wedge\mathrm{\small ELIM/1}}) \quad \cfrac{A \wedge B}{B}~\color{blue}{(\wedge\mathrm{\small ELIM/2})}$$ $$ \cfrac{A}{A \vee B}~\color{blue}{(\vee{\mathrm{\small INTRO/1}}}) \quad \quad \frac{B}{A \vee B}~\color{blue}{(\vee{\mathrm{\small INTRO/2}})} $$ $$ \cfrac{\begin{array}[cc]{} \\ {} \\ A \vee B \end{array} \quad \begin{array}[cc]{} [A] \\ ~~\vdots \\ \phantom{[}C\phantom{]} \end{array}\quad \begin{array}[cc]{} [B] \\ ~~\vdots \\ \phantom{[}C\phantom{]} \end{array} } {C}~\color{blue}{(\vee{\mathrm{\small ELIM}})} $$ $$ \cfrac{\begin{array}[cc]{} [A] \\ ~~\vdots \\ \bot \end{array} }{\neg A}~\color{blue}{(\neg{\mathrm{\small INTRO}})} \quad \cfrac{A \quad \neg{A}}{\bot}~\color{blue}{(\neg{\mathrm{\small ELIM}})} $$ $$ \cfrac{ \begin{array}[cc]{} [A] \\ ~~\vdots \\ \phantom{[}B\phantom{]} \end{array}}{A \rightarrow B} ~\implintro % % -> ELIM % \quad \quad \frac{A \rightarrow B \quad A}{B}~\implelim $$ $$ \cfrac{\bot}{A}~\botelim $$

Each rule preserves validity, which ensures that derivations will produce correct results (soundness). If one does not consider the proof-theoretical explanation of what an inference rule is as sufficient, one needs to talk about models and interpretations.

Moreover the collection of rules is systematic in a different way: if we ignore the duplicity of $\color{blue}{(\wedge{\mathrm{\small ELIM}})},\color{blue}{(\vee{\mathrm{\small INTRO}})}$ rules, we can say: for every logical operator $\neg, \wedge, \vee, \rightarrow$ there is one introduction rule and one elimination rule. In a sense, the introduction rule defines the meaning of the operator, and the elimination rule is ultimately a consequence of this definition: it removes precisely what was introduced! These are the "detours" in the structure of proofs, which can be removed.

In order to avoid unnecessary complication, we need to convene that in rule $\notelim$, the conclusion $A$ is always different from $\bot$. If we omit the rule $\notelim$, we end up with minimal logic. Let us now take two rules and read what they are saying:

• $\andelimleft$ is the (left) elimination rule for $\wedge$, and says: if you have a proof of $A \wedge B$, then you also have a proof of $A$
• $\andintro$ is the introduction rule for $\wedge$, and says: if you have a proof of $A$ and a proof of $B$, you may combine them into a proof of $A \wedge B$.

Assumptions. As mentioned, a derivation may start in any formula $A$ at the leafs. In the course of the proof, the assumptions may be discharged, as seen in the inference rules $\color{blue}{(\rightarrow{\mathrm{\small INTRO}})}$, $\color{blue}{(\neg{\mathrm{\small INTRO}})}$ and $\color{blue}{(\vee{\mathrm{\small ELIM}})}$. The discharged assumption is then marked $[A]$ to indicate that the conclusion does not depend on it. The rule $\color{blue}{(\rightarrow{\mathrm{\small INTRO}})}$ says if you can prove $B$ from assumption $A$, then we have proven from $A$ follows from $B$, i.e. $A \rightarrow B$. Note that it is possible that there are several other, undischarged assumptions still present in the derivation, and that the discharged assumption may have occurred multiple times in the subderivation, with all those occurrences being discharged at once.

Let's go through an example proof of $X \vee (Y \wedge Z) \rightarrow (X \vee Y) \wedge (X \vee Z)$. For this, we will need a derivation that ends in $\implintro$. $$ \cfrac{ \begin{array}[cc]{} [X \vee (Y \wedge Z)] \\ ~~\vdots \\ (X \vee Y) \wedge (X \vee Z) \end{array} }{ X \vee (Y \wedge Z) \rightarrow (X \vee Y) \wedge (X \vee Z) }{\implintro} $$ For the upper part, we need $\orelim$. $$ \cfrac{ \begin{array}[cc]{} {\phantom{X}} \\ {\phantom{\vdots}} \\ X \vee (Y \vee Z) \end{array} \quad \begin{array}[cc]{} [X] \\ ~~\vdots \\ (X \vee Y) \wedge (X \vee Z) \end{array} \quad \begin{array}[cc]{} [Y \wedge Z] \\ ~~\vdots \\ (X \vee Y) \wedge (X \vee Z) \end{array} }{ (X \vee Y) \wedge (X \vee Z) }{\orelim} $$ The two branches are now easy: $$ \cfrac{\cfrac{X}{(X \vee Y)}\orintro\quad\cfrac{X}{(X \vee Z)}\orintro} {(X \vee Y) \wedge (X \vee Z)}{\andintro} $$ $$ \cfrac{\cfrac{\cfrac{Y \wedge Z}{Y}\andelimleft}{(X \vee Y)}\orintro\quad\cfrac{\cfrac{Y \wedge Z}{Z}\andelimright}{(X \vee Z)}\orintro} {(X \vee Y) \wedge (X \vee Z)}{\andintro} $$

Intuitionistic treatment of negation. What if we treated $\neg A$ as an abbreviation for $A \rightarrow \bot$? Then the the role of $\color{blue}{(\neg{\mathrm{\small INTRO}})}$ is played by $\color{blue}{(\rightarrow{\mathrm{\small INTRO}})}$ and the role of $\color{blue}{(\neg{\mathrm{\small ELIM}})}$ is played by $\color{blue}{(\rightarrow{\mathrm{\small ELIM}})}$. In fact, every derivation in the language with primitive $\neg$ could be rewritten into a derivation for the language where $\neg$ is an abbreviation. Neat!

Normal form. A natural deduction proof is said to be in normal form if there is no detour, i.e. if there is no formula that is both the conclusion of an introduction rule and at the same time a major premise of an elimination rule. This is due to what Prawitz calls the inversion principle: whenever there is an elimination rule which operates on the result of an introduction rule above, then the results of that elimination rule were already present among the premises of the introduction rule. A normal derivation will - roughly - take apart the assumptions at the leaves with elimination rules and then build up the conclusion with introduction rules. (The $\orelim$ rule complicates this a little, since it passes through a formula $C$ from its minor premises; the proof by induction on the structure of derivations will transform such proofs by rewriting them and push the application of $\orelim$ downwards).

Curry-Howard correspondence. As discussed last time, we can assign terms of simply-typed $\lambda$-calculus to these derivations. Propositions of IPC are then exactly the types of simply-typed $\lambda$-calculus, with $\wedge$ product types and $\vee$ for sum (coproduct) types. Or, from the vantage point of logic, $\lambda$-terms are proof terms. Normalization of proofs corresponds to normalization of $\lambda$-terms; $\beta$-reduction corresponds to removal of a detour involving $\implintro$ and $\implelim$.

Still on Curry-Howard, it's a bit less obvious how to interpret $\botelim$ as a typing rule; the answer is that it needs an $\mathsf{abort}$ constant which (similar to throwing an exception) passes control to an imaginary top level function that never terminates. This and more is explained succinctly in Zena Ariola's slides [8], but I do want to point out how this yields a neat programmer's intuition for the convention regarding $\botelim$: since obviously an program $\mathsf{abort}(\ldots(\mathsf{abort}(t)\ldots)$ could always be replaced by a simple $\mathsf{abort}(t)$.

[8] Zena Ariola. The interplay between logic and computation. slides from a talk at "Women in Logic 2019".

Natural deduction in sequent calculus style

There is something odd about the above presentation: we have propositions at the leaves of a derivation which are temporarily treated as assumptions and then cease to be assumptions when they are discharged. It is also possible to not discharge them, or discharge only some of them when making a proof step. Here, we present an alternative formulation that makes it clear what happens with assumptions at every inference step.

(I thought for a long time that it was type theorists or programming language researchers who invented this, suspecting typographical reasons, but to my surprise I learned that it was in fact Gentzen [9] himself in 1936 who introduced this alternative in the paper where he proved the consistency of Peano arithmetic using transfinite induction.)

We shall present now intuitionistic natural deduction "in sequent calculus style". Derivations are still tree-shaped, however instead for formulas, premises and conclusions are sequents of the form $\Gamma \vdash A$ where $\Gamma$ is a (possibly empty) set of formulae. The meaning of a sequent is "from assumptions $\Gamma$, one can (intuitionistically) prove $A$". We write the union of such sets with a comma, omit braces around singleton sets and treat $\neg A$ as abbreviation for $A \rightarrow \bot$ so we don't have to give any additional rules. Then, the rules look like this: $$ \cfrac{\Gamma \vdash A\quad \Delta \vdash B}{\Gamma, \Delta \vdash A \wedge B}~\color{blue}{(\wedge\mathrm{\small INTRO})} \quad \cfrac{\Gamma \vdash A \wedge B}{\Gamma \vdash A}~\color{blue}{(\wedge\mathrm{\small ELIM/1}}) \quad \cfrac{\Gamma \vdash A \wedge B}{\Gamma \vdash B}~\color{blue}{(\wedge\mathrm{\small ELIM/2})}$$ $$ \cfrac{\Gamma \vdash A}{\Gamma \vdash A \vee B}~\color{blue}{(\vee{\mathrm{\small INTRO/1}}}) \quad \quad \frac{\Gamma \vdash B}{\Gamma \vdash A \vee B}~\color{blue}{(\vee{\mathrm{\small INTRO/2}})} $$ $$ \cfrac{\Gamma \vdash A \vee B \quad\quad \Delta, A \vdash C \quad\quad \Theta, B \vdash C}{\Gamma, \Delta, \Theta \vdash C}~\color{blue}{(\vee{\mathrm{\small ELIM}})} $$ $$ \cfrac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B}~\implintro % % -> ELIM % \quad \quad \cfrac{\Gamma \vdash A \rightarrow B \quad \Delta \vdash A}{\Gamma, \Delta \vdash B}~\implelim $$ $$ \cfrac{\Gamma \vdash \bot}{\Gamma \vdash A}~\botelim $$

These rules make it clear that it is now "compulsory" to discharge assumptions. When a rule has multiple premises, the assumptions are combined. By choosing broad enough set of assumptions ahead of time (weakening) the different sets of assumptions can be assumed to be the same. When moving towards sequent calculus, one can do away with the treatment of assumptions as sets and treat them as ordered sequences but with structural rules like exchange and contraction; removing one or both structural rules then yields sub-structural logic and proof theory.

[9] Gerhard Gentzen (1936) "Die Widerspruchsfreiheit der reinen Zahlentheorie"

Conclusion

We are at the end of our tour; I hope this can provide a good starting point for studying the multiple connections between $\lambda$-calculus, logic and proof theory.

Sound reasoning - preferably automated - and some form of formal logic and proof are going to be key when modeling some domain and constructing correct software for it. Programmers are used to deal with precise formulations (programming languages, specs) but only a subset will be interested in the "formalization of all mathematics"; a programmer with a basic understanding of simply-typed $\lambda$-calculus should ideally have a very clear path to understanding logic, proof assistants, type theory - I don't think that this is the case today.

The activities in constructing models and software may be similar to mathematics, but they are certainly not the same. Each domain is a mathematical universe, with random and often contradictory pieces of information waiting to be organized in "islands of consistency". Hopefully we will one day reach some widespread understanding and usable tool support for formal reasoning that can serve both practical informatics as well as formalizing mathematics.

[If you want to discuss, the HN thread is a great place to leave comments]

Higher-order Logic and Equality.

In this post, I want to sketch a particular perspective on $\lambda$-calculus and higher-order logic and Church's simple theory of types. I have a few motivations to write this up. One of them is that as an undergrad (ages ago), upon encountering first-order predicate logic, I had endlessly wondered why one couldn't use "boolean functions" and something like functional programming for logic. It was only much later that I discovered Church's 1940 typed $\lambda$ calculus was in a sense, just that.

When people think of the connection between $\lambda$-calculus and logic, the first thing that comes to their mind may well be the Curry-Howard correspondence. Similarly, the first thing that people may think of when hearing type theory is Martin Löf type theory. So another motivation is to have a place that describes higher-order logic a.k.a. simple type theory - which after all was the first appearance of typed $\lambda$ calculus - and how there are multiple ways to relate it to formal logic and proofs.

Preliminary: Natural Deduction

Natural deduction [wikipedia], in short, is a system of reasoning involving inference rules to derive new true statements from existing ones. What sets them apart from a Hilbert system [wikipedia] is that logical operators themselves are described using inference rules, proofs are trees (derivations) formed from such rule.

In this journey, we present natural deduction rules in sequent calculus style: assumptions are tracked in a context $\Gamma$.

Minimal Logic

Minimal logic [wikipedia], also referred to as the positive fragment of intuitionistic logic, is a deductive system for propositional logic that does not contain any inference rule for falsehood. Here are the rules: $$ \frac{}{\Gamma, A \vdash A}\quad\quad \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} $$ $$ \frac{\Gamma \vdash A \rightarrow B \quad \Gamma \vdash A}{\Gamma \vdash B}$$ We could have added conjunction $\wedge$ or disjunction $\vee$ or a symbol $\bot$ to stand for a false proposition, along with the convention that $\neg A = A \rightarrow \bot$; it would still be minimal logic. "Full" intuitionistic logic has a rule that goes from $\bot$ to an arbitrary proposition $A$ (ex falso quodlibet); and other rules, like double negation elimitation, get us classical logic.

The naming scheme that calls this "minimal" is consistent with Dag Prawitz's "Natural Deduction: A Proof-Theoretical Study." Yet, I believe it is fairly common to call this kind of logic intuitionistic logic, even though there is no rule for $\bot$.

The proofs for this logic have a structure that is familiar to all students of functional programming languages.

Simply typed $\lambda$-calculus

We now follow the celebrated "propositions-as-types" or Curry-Howard correspondence and assign names (variables) to assumptions, terms (expressions) to proofs, using this language: $$ s, t ::= x \enspace \vert \enspace (\lambda x: T. t) \enspace \vert \enspace(s\ t) \enspace $$ $$ T ::= b_i \enspace \vert \enspace T \rightarrow T $$

Here $b_i$ are some given base types. Our annotated inference rules: $$ \frac{}{\Gamma, x:A \vdash x:A}\quad\quad \frac{\Gamma, x:A \vdash s:B}{\Gamma \vdash (\lambda x:A. s) : A \rightarrow B} $$ $$ \frac{\Gamma \vdash s:A \rightarrow B \quad \Gamma \vdash t:A}{\Gamma \vdash (s\ t):B}$$ A term encodes the entire derivation (or natural deduction proof) of the proposition/type.

Reduction as proof normalization

From the Curry-Howard angle, functional programming is "proof normalization": derivations that contain redundant steps get simplified to smaller derivations. The redundancy is always of the form that part of the derivation needs an assumption $x:A$, and another part of the derivation actually "produces" a term of type $A$. In more detail, consider a derivation $\Gamma \vdash (\lambda x:A. s): A \rightarrow B$ and a derivation $\Gamma \vdash t: A$, which can be combined to yield $\Gamma \vdash ((\lambda x:A. s)\ t) : B$. The detour can be removed by taking every occurrence of $x$ within $s$ and replacing it with $t$. This yields a smaller derivation $\Gamma \vdash s[t/x] : B$. If two derivations stand in this relation, we call them $\beta$-equivalent. $$ ((\lambda x:A. t)\ s) \approx_\beta t[s/x] $$

Here $[s/x]$ is notation for substituting $s$ for $x$, and we hurry to point out that care must be taken that we may need to rename bound variables. Two terms that only differ in the names of their bound variables are $\alpha$-equivalent and we will pretend they are equal. If we used de Bruijn indices instead of variable names, there would be no need for $\alpha$-equivalence.

[Digression: the identity above is not an algebraic identity - these are syntactic objects which involve variable binding. Sometimes it is ok to treat lambda-calculi as an algebra, and this leads to combinatory logic, see neelk's answer on stackexchange and Selinger's paper.]

If we give a direction to the identity, we obtain $\beta$ reduction: $$((\lambda x:A. t) s) \Rightarrow_\beta s[t/x]$$ We can show that $\Rightarrow_\beta$ is strongly normalizing and therefore terminating reduction relation, and that $\Rightarrow_\beta$ is confluent (Church-Rosser property), so all reductions end up in the same normal form. This yields a decision procedure for the "word problem": to find out whether $s \approx_\beta t$, reduce both to normal forms and check that they are equal.

We now shift our perspective, leave the Curry-Howard correspondence aside and look at the theory of equality between these expressions. \(\newcommand{\qeq}[0]{\color{blue} {\mathrm{eq}}}\)

Higher-order Logic, using Equality alone

We are going to build a calculus for classical logic, based on our language. Our development here follows the $Q_0$ type theory (due to Peter Andrews). This is a type theory which is close to Church's 1940 simply-typed $\lambda$ calculus, but uses only equality and a description operator. We will omit the description operator.

We need two base types: $\iota$ for "individuals" and $\omicron$ for "propositions". Since the logic is classical, every proposition will be either true of false, so $\omicron$ can be seen as the type these "truth values". With this setup, we can view any term of type $\iota \rightarrow \omicron$ as describing a set of individuals, or alternatively, a predicate. This resembles the characteristic function of a set in mathematics and also what a programmer calls a Boolean function.

[ The name "higher-order" is appropriate, since this logic lets us also talk about set of sets of individuals, via terms of type $(\iota \rightarrow \omicron) \rightarrow \omicron$ and so on. This use also matches the terminology "higher-order function", which is not a coincidence. Note that you can quantify over "smaller-order predicates", but you can't express a "set of all sets."]

The only built-in/primitive notion is a logical constant $\qeq_\alpha: \alpha \rightarrow \alpha \rightarrow \omicron$ which serves as equality operator for any type $\alpha$. Before we build propositions out of logical operators and quantifiers, let us write down types of such operators, with the common convention that $\alpha \rightarrow \beta \rightarrow \gamma$ stands for $\alpha \rightarrow (\beta \rightarrow \gamma)$ the types would be: $$ \newcommand{\qtrue}[0]{{\color{blue} {\mathrm{true}}}} \newcommand{\qfalse}[0]{{\color{blue} {\mathrm{false}}}} \newcommand{\qnot}[0]{{\color{blue} {\mathrm{not}}}} \newcommand{\qor}[0]{\color{blue} {\mathrm{or}}} \newcommand{\qand}[0]{\color{blue} {\mathrm{and}}} \newcommand{\qimplies}[0]{\color{blue} {\mathrm{implies}}} \begin{align*} \qtrue:\ & \omicron\\ \qfalse:\ & \omicron\\ \qnot:\ & \omicron \rightarrow \omicron\\ \qand:\ & \omicron \rightarrow \omicron \rightarrow \omicron\\ \qor:\ & \omicron \rightarrow \omicron \rightarrow \omicron\\ \qimplies:\ & \omicron \rightarrow \omicron \rightarrow \omicron\\ \end{align*} $$ Using again a notational convention that $((r~s)~t)$ is written $r~s~t$, the tautology $A \vee B \rightarrow B \vee A$ is expressed as $\qimplies~(\qor~A~B)~(\qor~B~A)$.

What about quantifiers? Since we have $\lambda$, for variable binding, there is no need for other variable binders like $\forall$ or $\exists$. Instead we introduce universal and existential quantification using two higher-order operators: $$ \newcommand{\qPi}[0]{\color{blue} \Pi} \newcommand{\qSigma}[0]{\color{blue} \Sigma} \begin{align*} \qPi_\alpha:\ & (\alpha \rightarrow \omicron) \rightarrow \omicron\\ \qSigma_\alpha:\ & (\alpha \rightarrow \omicron) \rightarrow \omicron\\ \end{align*} $$ So $\forall x .\exists y. x = y$ would be expressed as $\qPi \lambda x. \qSigma \lambda y. \qeq~x~y$. People studying classical logical systems frequently "apply Occam's razor" and try to define as few thing as possible. The $Q_0$ way is to play Occam's razor as much as possible. All logical operators are "implemented" using only $\qeq$. $$ \newcommand{\tprop}[0]{\omicron} \begin{align*} \qtrue &:= \qeq_{\tprop \rightarrow \tprop \rightarrow \tprop} \qeq_\tprop \qeq_\tprop\\ \qfalse &:= \qeq_{\tprop \rightarrow \tprop} (\lambda x:\tprop. \qtrue) (\lambda x:\tprop. x)\\ \qnot &:= \qeq_{\tprop \rightarrow \tprop} \qfalse\\ \qand &:= \lambda x:\tprop. \lambda y:\tprop. \\ &\quad \quad \qeq_{\tprop \rightarrow \tprop \rightarrow \tprop} \\ &\quad \quad \quad (\lambda z: \tprop \rightarrow \tprop \rightarrow \tprop. z~\qtrue~\qtrue) \\ &\quad \quad \quad (\lambda z: \tprop \rightarrow \tprop \rightarrow \tprop. z~x~y) \\ \qor &:= \lambda x:\tprop. \lambda y:\tprop. \\ &\quad \quad \qnot~(\qand~(\qnot~x)~(\qnot~y))\\ \qimplies &:= \lambda x:\tprop. \lambda y:\tprop. \qeq~x~(\qand~x~y)\\ \qPi_\alpha &:= \qeq_{(\alpha \rightarrow \tprop) \rightarrow (\alpha \rightarrow \tprop) \rightarrow \tprop}~(\lambda x : \alpha. \qtrue)\\ \qSigma_{\alpha} &:= \lambda x: \alpha \rightarrow \tprop. \qnot~~\qPi_{\alpha}~~\qnot~x.\\ \end{align*} $$

One advantage of having everything defined in terms of $\qeq$ is that when we give inference rules to explain how reasoning take place, they all involve only $\qeq$. We are using the notation of inference rules to describe an equational theory. The only assertions $\Gamma \vdash r$ that are derived are (more or less - up to $\beta$-equivalence) of the form $\Gamma \vdash \qeq_\alpha~s~t$, but we explicitly write some assumptions that we make about types. Here they are: $$ \frac{\Gamma \vdash s : \tprop \rightarrow \tprop}{\Gamma \vdash \qeq_\tprop~(\qand~(s~\qtrue)~(s~\qfalse))~(\qPi_\tprop~\lambda x : \tprop.~s~x)} $$ $$ \frac{\Gamma \vdash s : \alpha \quad \Gamma \vdash t:\alpha \quad \Gamma \vdash z: \alpha \rightarrow \tprop}{\Gamma \vdash \qimplies~(\qeq_\alpha~s~t)~(\qeq_\tprop~(z~s)~(z~t))} $$ $$ \frac{\Gamma \vdash s : \beta \rightarrow \alpha \quad \Gamma \vdash t:\beta \rightarrow \alpha}{\Gamma \vdash \qeq~(\qeq_{\beta \rightarrow \alpha}~s~t) (\qPi_\alpha \lambda x:\alpha.\qeq_\alpha~(s~x)~(t~x))} $$ $$ \frac{}{\Gamma \vdash \qeq~((\lambda x : \alpha. s)~t)~(s [t/x])} $$ $$ \frac{\Gamma, x: \alpha \vdash r : \beta \quad \Gamma \vdash r[A/x] \quad \vdash \qeq_\alpha~A~B}{\Gamma \vdash r[B/x]} $$

The first rule is an axiom that says $\tprop$ consists of $\qtrue$ and $\qfalse$. This looks like a data type specification for $\tprop$. The second rule is an axiom that says that if two objects are equal then they have the same properties (Leibniz would say "indiscernibility of identicals"). The third rule is an axiom that says two expressions of function type are equal, if they agree on all arguments; this is the extensional definition of function equality.

The fourth rule is an axiom for $\beta$-conversion. We're conveniently hiding all the naming stuff again behind $[t/x]$ notation; but essentially this lets us apply $\beta$-reduction as we please.

The fifth rule is a proper inference rule - the only actual inference rule, which has a premiss $\Gamma \vdash r$ - that says "equals can be replaced by equals", anywhere in a term. This is where the actual reasoning happens. For example, a proposition $\forall x:\alpha. P$ is encoded as a $\qPi \lambda x:\alpha. P$ and proving it "within the system" is literally showing that $\lambda x:\alpha. P$ is equal to $\lambda x:\alpha. \mathsf{true}$.

Wrapping up

I presented in a notation/style that is different from both Andrews's book or the Stanford Encyclopedia of Philosophy's entry on Church's type theory. It is closer to the way a typed programming languages would be formulated.

We have only scratched the surface, but sketched how a whole formal system of reasoning can indeed be based on $\lambda$ calculus playing the role of characteristic function. And it didn't actually involve Curry-Howard correspondence. I like to think of this situation as "multiple levels of logic," and topics like higher-order unification and meta-logic/logical frameworks make use of this.

I hope these notes can help raise awareness for what is going when simple type theory and higher order logic. A lot more can be said, but that is for another post. If you are interested to dive deeper, here are some references that talk about higher-order logic.

  Stanford Encyclopedia of Philosophy's entry on Church's type theory

  Jean Gallier. "Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi", freely accessible on his logic papers page.

  William M. Farmer "The Seven Virtues of Type Theory" https://doi.org/10.1016/j.jal.2007.11.001

  Peter Andrews "An Introduction to Mathematical Logic and Type Theory: to Truth through Proof" (2002)

  Alonzo Church. "A Formulation of the Simple Theory of Types". J. Symb. Logic, 5 (1) (1940)

  Dag Prawitz. "Natural deduction: A Proof-Theoretical Study" (2006) Dover - new issue of the celebrated 1965 work.

Getting from TikZ to PNG

For things like papers, tutorials, books, LaTeX is still where it's at, but for HTML I'd like to be able to do things like commutative diagrams... how to make this work without duplicating effort? My LaTeX foo has become rusty over the years, but despite much searching, there seems to no alternative. So here is a little note on how to TikZ pictures to PNG.

TikZ for drawing diagrams

TikZ (TikZ is kein Zeichenprogramm) is probably the most powerful LaTeX package to graphics. There are supporting packages for commutative diagrams.

Exporting TikZ to PNG

After some searching I found the following way: use the "standalone" document class...

\documentclass{standalone}
\usepackage{tikz}
\usetikzlibrary{cd}
\begin{document}
\begin{tikzcd}
        & X \arrow[dl] \arrow[d, dotted] \arrow[dr] & \\
        A & A \times B \arrow [l] \arrow{r}& B
\end{tikzcd}
\end{document}

... together with the convert tool (imagemagick):

product.png: product.tex
        pdflatex $<
        convert -density 600x600 product.pdf \
           -quality 90 -resize 1080x800 -strip $@

The product

And this is what we get:

Taking a Glance at Containers, Packages and Development

Time to dust off this blog.

Long time ago, I had worked on (yet another) open source implementation of a RPC plugin (code generation + client/server framework) for handling the "services" that are part of protobuf. I had briefly looked at existing C++ solutions, but I remember I primarily cared about finding out what it would take. I looked for ages for a suitable build tool, ultimately settling on gyp and ninja. And then, I still needed to handle dependencies.

At some point I must have lost interest, many years have passed, Bazel was meanwhile open-sourced. What (subjectively) changed more than anything else was that the world has moved on, docker containers, cloud setups are becoming more the standard than the norm, the word "DevOps" was invented, kubernetes is a thing. So people must have a way to deal with APIs. There is something called Swagger which can document APIs and also generate client and server-side code, with many languages and targeting language-specific frameworks...

Docker for Development

Apart from the revolution that this means for operations and delivery, this led me to think that a key development story is addressed this way, namely declaring dependencies and integrating them into the build process. Indeed I found a nice article by Travis Reeder that describes exactly the advantages, along with helpful examples and command line references.

Build tools, Modularity and Packages

Modularity is pretty much essential to serious development. I remember from university times that academic view on modularity seemed primarily from an angle of programming languages (in the old times, "separate compilation", later, through type systems). Nowadays, nobody considers providing a programming language implementation in isolation, for instance Rust has the notion of crates and modules, and what's more is that the cargo tool to manage crates is mentioned in the tutorial. npm would be another good example. In Java-land, there is a distinction between libraries on the class path and managing external dependencies using build tools like maven or gradle.

Just to state the obvious: the old view of considering modularity maybe as a low-level problem (linking and type systems) ignores the fact that a "modern" build tool has to handle package/module/crate repositories (multiple of them). On the other hand, the emergence of such repositories (plural) has its own problems, when "left-pad" package was pulled and broke many people. "npm disaster" is an entertaining search query, but it does lead to not-easily-resolved questions on the right granularity of modules/packages.

Image or Container?

With Docker as an emerging "modularity mechanism", it is very interesting to observe that in conversation (or documentation) people confuse docker image with a docker container. If you are confused, this post will get you on the right path again.

There is a parallel between a "module" as something that can be built and has an interface, and "module" as something that is linked and part of a running system. Since a container is a whole system in itself, networking is part of its interface. When building a larger system from containers as building blocks, the problem of connecting these requires tackling "low-level" configuration of an entirely different kind (see Kubernetes docs) than what "module linking" meant in the 80s. Still, I'd consider this a parallel.

Where are the best practices?

A quick search reveals that indeed there are 53k+ projects have Dockerfiles, including e.g. tensorflow, which explicitly mentions deployment and development Docker images. So while initially, I thought I had not slept through much essential changes, it seems on the contrary that things are happening at an entirely different level. What conventions should one follow, what are the pitfalls?

Fortunately for me, there are smart people good at posting articles about these things, so I can appreciate the problems and tentative solutions/best practices mentioned in Top 5 Kubernetes Best Practices. Hat-tip to the "Make sure your microservices aren’t too micro" advice.

D.C. al Coda

How can there be an end to this? Containerization seems to be a perpetual journey. At this point, I would have liked to offer tips based a "typical" example of a development project and how one would use docker to set up. However, I am not very active in terms of open source development, and the one project I want to get back to most isn't a developer tool at all. Fortunately, I believe best practices for "docker for development" aren't going to be any different from the best practices for using docker in general.

There is an interesting point where, in order to build a container image, one has to still solve the problem of gathering the dependencies. So the problem of gathering dependencies at build time has only been shifted on level (up? down?), though the constraints are very different: an organization can find easy ways to make docker images available to their developers, and only the team that takes care of providing the docker image has to gather the dependencies. This appears to me much more sane than having a development workflow that makes connections to external repositories on the developers box at build time.

Web Components and Dart Frameworks

Recently, I visited the scientific software and data management (SSDM) group at ETH to give a talk about web components and dart frameworks. Here is a summary.

Looking back: a brief History of Web Apps

We live in interesting times: there are many frameworks, languages out there, and in order to understand the context and why things are how they are, it helps to look at the history. The web as a platform for applications has evolved in an erratic process, which I will divide into three broad phases:

• the "Middle ages": content generated on the server-side, Java born with the promise of applets, Javascript launched as a tool for web designers (read: non-programmers), browser wars [1]. Client-side coding was a matter of achieving visual effects, client-server communication happened through forms and page-loads.
• the "Renaissance": asynchronous Javascript[2] becomes ubiquitous, client-server communication is now decoupled from forms and page-loads. Rich client-side apps like GMail or Google Maps demonstrate its use.
• "Modern History": high-performance layout and javascript engines are the norm. HTML5 delivers a reinterpretation of browser documents and APIs, tailored to web applications development. Mobile devices get high resolution screens and useful browsers.

HTML5 continues to evolve, and not all HTML5 technologies are not supported on every browser (so developers check on caniuse.com). The idea of a Polyfill is born: adapter code that simulates functionality that does not exist natively in the browser.

Web Components

With application development on the web becoming the norm, the traditional questions of software engineering arise: how to approach development of large systems? how to encapsulate and reuse? Web components [3,4] offer an answer.

Web Components are four technologies that together achieve reusable units of behavior:

• custom elements
• templates
• shadow DOM
• HTML imports

These technologies are being standardized and implemented in a few browser. Even when not available natively, there is the possibility of using polyfills.

As with any web technology, there are good documentation resources available on the web that explain these. In the following, I'll just include a simple example for completeness.

Defining a new custom element

Say we want to write a bug-tracking system that displays a number of bug entries. We'd like to treat the entries as we would treat other HTML elements (note the fancy new HTML5 syntax):

  <bug-entry bug-id=1e4f bug-status=open>

This is possible with custom elements, we'd want to register the element like so:

// Create a new object based of the HTMLElement prototype.
var BugEntryProto = Object.create(HTMLElement.prototype);

// Set up the element.
BugEntryProto.createdCallback = function() {
  ...render bug entry, e.g. with img, click handler/link
}
// Register the new element.
var BugEntry = document.registerElement('bug-entry', {
    prototype: BugEntryProto
});

Filling the element with content

Most of the time, custom elements will actually correspond to some other markup. With HTML templates, it is possible to include template markup in documents and instantiate it.

<template id=”bug-entry-template”>
  <tr><td><img class=”bug-image”></td>
      <td><div class=”bug-title”></td></tr>
</template>

BugEntryProto.createdCallback = function() {
  … 
  var template = document.querySelector('#bug-entry-template');
  var clone = document.importNode(template.content, true);
  …
}

Specifying layout and style of the content

In HTML, layout and style is specified using CSS, however the specification is global. In order to have a self-contained, encapsulated unit of code, we need some mechanism that enables reuse without worrying about style. This is what is achieved with the shadow DOM: content can be added to the DOM in a way that keeps it separate from the rest of the DOM.

BugEntryProto.createdCallback = function() {
  // create shadow DOM 
  var root = this.createShadowRoot();

  // Adding a template
  var template = document.querySelector('#bug-entry-template');


  var clone = document.importNode(template.content, true);
  …
  root.appendChild(clone);
}

Importing the new component

The sections above have defined a component. Now we would like to be able to use the component. HTML imports provide a way to import components easily:

<link rel="import" href="bug-entry.html">

Dart Frameworks

Polymer

The Polymer.js library provides many things:

• Polyfills to get web components in browsers that don't support them
• Many ready-to-use components that follow Material Design UX specifications
• Tools like vulcanize that translate away HTML imports for the purposes of deployment

The polymer.dart library is a wrapper around polymer.js that makes the polyfill as well as the components available in dart. It also offers an easy, integrated syntax which is mainly possible because of reflection. Instead of using vulcanize, users of polymer.dart rely on the polymer transformer which translates away the use of reflection and also takes care of combining all the imported components into one unit of deployment.

There is a bottom-up development approach suggested by the availability of polymer: start building basic components and assemble them into every larger ones until you have an application. It is important to note that polymer is not an application development framework: things like logical pages, views, routing are not standardized, but can be provided by components.

Angular, Angular.dart and Angular2

Angular existed before web components and polymer. It was always a framework for application development, so provides facilities for pages, views, routing. The dart version of angular is significantly different from the js version, again because the use of reflection permits a nice style that uses annotations. Angular does not work seamlessly with web components defined in polymer, although it is possible to make the two things work with a bit of glue code.

The newer version, angular2, is backwards incompatible with angular (though concepts are similar). It aims to provide seamless integration of web components (as defined by the standard). It is noteworthy that annotations are advocated as the primary means to set up angular2 components.

Conclusion

Web development has become even more interesting with the promise of reusable, encapsulated components. Work on these is still in progress, but I for one am looking forward to more structured web applications that can draw from a large set of reusable components.

References

[1] Brendan Eich interview in InfoWorld, 2008
[2] https://en.wikipedia.org/wiki/Ajax_(programming)
[3] Web Components description in Mozilla Developer Network
[4] https://en.wikipedia.org/wiki/Web_Components
[5] Are we componentized yet?

Educational Programming Environments for Children

If one considers programming a passion, then one can endlessly search for the "essence" of programming. Sooner or later, one faces the question: how can something as abstract as programming be taught to children? What will we teach our children?

This is a broad topic, so I will focus on describing some programming environments that I saw being used at educational events at the Google Zurich office. The usual disclaimer applies: the opinions herein reflect only my personal point of view, not necessarily that of Google.

Background and Setup

At the Google Zurich office, we occasionally organize events that teach (or rather: expose) programming to children. The occasion / program and audience were slightly different each time but what is common is the goals of supporting STEM education, closing the gender gap in CS, and at one of the events also giving kids an impression of what their parents are doing ... basically showing them that this stuff is fun. Note that this wasn't a controlled experiment of any sort - my comparison of the environments we used is more an afterthought.

I have participated in a few of these as facilitator and seen how three educational programming environments were applied in practice and I want to share a quick overview in the hope that it is useful for future events of this kind. These were:

• Logo,
• Agent Cubes, and
• Scratch.

All three environments were used in their online variant in the context of educational events organized for groups of kids: 30-40 Chromebooks and a bunch of volunteers to help in case of questions. Many times, a single child would get a machine of their own, but we also did groups of 2-3. Sometimes we would spend some time briefing the volunteers, but this was pretty minimal.

Logo

This event was a 2h workshop and took place in November 2012. I was the main facilitator for it, and had previously written a logo interpreter ArrowLogo in my 20% time (*). I have also used it to discuss programming in a 30 minute session with a group of school children visiting the office in January 2015.

(*) I used to code in logo when I was a kid myself. There are other, Java-based Logo implementations available e.g. xlogo, but note that using these would require installation of a desktop app, or enabling Java plugin in a web browser. Installing desktop apps is often not an option (e.g. Chromebooks won't allow this), and enabling the Java plugins often turned out to be a security hazard in the past.

Logo was invented by Seymour Papert and others in 1967. The design of Logo is deeply rooted in constructivist learning and his Papert's book "Mindstorms: Children, Computers, and Powerful Ideas" is a very accessible resource that explains well how its creator viewed it as a tool not to teach programming but to approach education in general.

The summary is this: children are exploring the environment, essentially teaching themselves. The "teaching yourself" part will resonate with every programmer. LOGO achieves this by providing a facility for turtle graphics: kids need to instruct the turtle where to move in order to create paintings that way. This is simple procedural (imperative) programming.

For practical purposes, in a short workshop one will usually want to provide exercises to give some structure to the session; I was able to use LOGO teaching resources from ABZ, a group at ETH Zurich that is promoting informatics education for young kids. For beginners, it is very easy to come up with turtle graphics exercices: you can draw triangles, boxes, houses and move on to circles, flowers, filled box, colored paintings.

Something notable about Logo is that the childrens' activity is very close to what programmers do: manipulate source code in textual representation, run, even "debug". It also means that some basic typing skills and being able to navigate a very simple graphical user interfaces with a mouse are requirements.

Learning the ArrowLogo environment is very easy because it is very basic: there is a graphics panel, some place to write the code, and some commands to control what is happening, and that is it. The turtle graphics provides immediate feedback, and it is very easy to start over, giving children motivation to sort things out by themselves. After a short lead time, children seemed to be able to use the environment fine.

On the other hand, there are no fancy images or sounds, and building interactive things or games was out of scope. Also, ArrowLogo does not provide a way to save programs or take them home; since most programs written in this short time where basic and easy to reproduce, this did not seem to be a shortcoming.

Scratch

This even took place in March 2015, the audience was young girls (ages 10-12) and each of them had their own chromebook. They accessed scratch.mit.edu with profiles that were created ahead of time (some confusion arose since some tried to treat their scratch profile intro as a (Google-) account).

Scratch is developed by the MIT media lab, which is a successor to the group that created Logo. Scratch offers a visual programming editor: kids can create and customize actors and control them through scripts. The scripts are not coded as textual source code, but by combining blocks by using drag-and-drop.

The user interface is complex. There is almost no typing needed, except for entering values; however a good command of a mouse and a good understanding of graphical user interface is essential and this was clearly a problem for some of the participants.

Scratch is fascinating for kids, because it enables them to do game or animation development. However, it is also a moderately complex environment to learn, and if one is not ready to deal with this complexity, then the insights into programming that children can get are quite limited.

I showed kids how they could add keyboard control for their actors or automate their movement, but I feel that at least with some part of the childen, there was no understanding for what is happening and why, and no engagement. With such a complex environment, it is easy to fall back into an "instructionist" pattern and tell kids every single step they need to take and ask them to mechanically repeat it. Alternatively, one can accept that some of the participants will be distracted by looking at different shapes, being obsessed with drawing things or playing sounds.

Kids could save their work, take their profile details home and continue. Though many said they would like to continue, I have some doubts.

Agent Cubes

Alexander Repenning visited Google to run an "Hour of Code" workshop in May 2014, using his software Agent Cubes Online.

Just as in scratch, the user can add agents and define behavior for them using rules. The focus is clearly on game design, and it is really easy to clone agents (e.g. think of the many trucks in the frogger game, all running the same code). The user interface for Agent Cubes Online however is even harder to get used to than scratch. There are too many buttons, most of them are too small. Like in scratch, there is a multitude of things that can be done, like draw your own agents.

The 'hour of code' was very structured: small demonstrations by the teacher would alternate with periods were kids were free to replicate the steps. Clearly, we have left any constructivist pretensions behind since the purpose is game design at all cost.

I think the level of engagement was clearly there, but it is hard to tell whether children would be able to "make it their own" later. Certainly, some kids enjoyed playing with the thing, but I don't think the majority of them thought of themselves as programmers or would return to game development.

Kids were able to save their work to their profile and could continue their work later. This required registering with their email address at the end of the workshop.

Conclusion: use code.org

My personal "conclusions" from all these were the following:

• for kids, visual programming can be quite helpful, because it is appealing and easier to use. I am looking forward to seeing such a session with a touch screen interfaces
• there seems to be a wide spectrum between turtle graphics and game development. "Flashiness" seems to be a factor in getting some kids engaged; or as the game development motto goes "[audiovisual] content is king"
• ArrowLogo is seriously lacking facilities for developing interactive things or animations.

While doing some research, I found there is a more convincing solution in this design space. The Google-developed blockly library for visual programming has been used at the code.org Hour of Code to create an introductory experience that easily beats all three environments that I described above; I mean: you can code turtle graphics by controlling a Disney(tm) character using visual programming blocks, and the character makes realistic ice-skating sounds as it moves!

I think if we take a step back, we will see that nothing can be concluded: it seems that the quest for the "right" answer will continue. I hope I have at least been able to shed some light on factors that contibute to successful intro-to-programming event for kids.

angular2 dart nested components

This is a quick post to share how to do nested components in angular2 dart. It is slightly expanded version of this stackoverflow answer. We start from the quickstart tutorial as follows: The index.html is unchanged:

<html>
  <head>
    <title>My App</title>
  </head>
  <body>
    <my-app></my-app>
    <script type="application/dart" src="main.dart"></script>
    <script src="packages/browser/dart.js"></script>
  </body>
</html>

In our main.dart file, we can reference components inside our templates as along as we also reference them in the directives field:

import 'package:angular2/angular2.dart';

// These imports will go away soon:
import 'package:angular2/src/reflection/reflection.dart' show reflector;
import 'package:angular2/src/reflection/reflection_capabilities.dart' show ReflectionCapabilities;

@Component(selector: 'graphics-panel')
@Template(inline: '<b>I am the graphics panel</b>')
class GraphicsPanel {}

@Component(selector: 'input-panel')
@Template(inline: '<i>I am the input panel</i>')
class InputPanel {}

@Component(selector: 'arrow-logo-app')
@Template(
  inline: '''
    <div><h1>Hello {{ name }}</h1> 
    <graphics-panel></graphics-panel>
    <input-panel></input-panel></div>
''',
  directives: const [GraphicsPanel, InputPanel]
)
class AppComponent {
  String name = 'Bob';
}

main() {
  // Temporarily needed.
  reflector.reflectionCapabilities = new ReflectionCapabilities();
  
  bootstrap(AppComponent);
}

cflags weirdness in gyp

I had posted a few hints for gyp and ninja usage a while ago. I still think this combination makes a great build system, but there are also a few weird things to mention. Found the solution on this gist thread and this question and answer on stackoverflow: if you want to specify c compiler flags or c++ compiler flags, you would to this via "xcode_settings". No comment.

{
  'make_global_settings': [
    ['CXX', '/usr/bin/clang++' ],
    # If you don't want to do this hack ...
    # ['CXX', '/usr/bin/clang++ -std=c++11' ],
  ],
  'targets': [
    {
      'target_name': 'shc',
      'type': 'executable',
      'sources': [
        # ... omitted
      ],
      # ... you would do this. It will work with the ninja generator.
      'xcode_settings': {
        'OTHER_CPLUSPLUSFLAGS': [
          '-std=c++11'
        ]
      }
    },
  ],
}

variables in gyp

These are the ways to set variables you can reference in your gyp files.

Variables are referenced using the expansion character '<', like so '<(foo)'.
This happens in ExpandVariables, see [input.py]. There is also an "expand to list" variant '<@', which works if the context expects a list and if the string being expanded does not contain anything else.
Here is a toy .gyp file that references a variable foo

{
  'targets': [
     {
       'target_name': 'foo_target',
       'type': 'executable',
       'sources': [ 'yo.c' ],
       'actions': [
          {
            'action_name': 'greet',
            'action': [ 'echo', 'hello world <(foo)', ],

            'inputs': [],
            'outputs': [ 'yo.c' ],
}]}]}

Now you could either add a variables section before 'targets' like so

'variables' : {
     'foo': 'bar'
  },

However, most of the time you will want to set these separately. You can do this in two ways.


1) include a separate file.
For this we would dreate a file some_vars.gypi that contains just this:

{
  'variables' : {
     'foo': 'bar'
  },
}      

and add an include to the original .gyp file

'includes': [ 'some_vars.gypi' ]

Here is the result:

$ GYP_GENERATORS=ninja gyp --depth=0 --toplevel-dir=`pwd` \
  simple_action.gyp 
$ ninja -C out/Default all 
ninja: Entering directory `out/Default'
[1/3] ACTION foo_target: greet
hello world bar
[...]

2) Set it on the command line.

gyp offers a "define" facility with the -D flag, which is also used to pass definitions down to the C/C++ compiler. The code says "-D is for default", so if the variable is already defined, that value is going to be used instead of your command line value.

Using the original .gyp file, we do

$ GYP_GENERATORS=ninja gyp --depth=0 --toplevel-dir=`pwd` \
  simple_action.gyp -Dfoo=baz
$ ninja -C out/Default all 
ninja: Entering directory `out/Default'
[1/3] ACTION foo_target: greet
hello world baz

For an example with list expansion, check out the [Actions example] in the gyp language spec.

gyp and ninja, hello world

Building software can be very complicated. Not writing the code, but just calling the various tools that will turn it into an executable.

For some time, I have been working on a 20% project that brought me back to the realm of open source development in C / C++. One thing that struck me is how many different build systems exist today. In this post, I just want to share a micro-tutorial on a particular combination.

* gyp - a meta-build system

* ninja - a tiny make-like build tool

These are children of the chromium project. For gyp, we describe targets in a high-level manner, with the option of platform-specific tweaks. Then a gyp "generator" will output platform specific build files (the choice includes xcodebuild, visual studio ...).

Given that gyp needs to have all the information necessary in order to generate build files, one does not really need a complicated lower-level build tool. Consequently, ninja is a minimal build tool that is lacking a lot of make's fanciness and flexibility, but enough to do the job.

Here now a sneak peek at how to use these two: assume I have a helloworld project like this.

helloworld.gyp
src/helloworld.cc


This is what the gyp file contains:

{
    'targets': [
    {
        'target_name': 'my_target',
            'type': 'executable',
            'sources': [
                'src/helloworld.cc',
            ],
    },
        ],
}

We can now use this then generates platform specific build files.

$ GYP_GENERATORS=ninja gyp helloworld.gyp --toplevel-dir=`pwd` --depth=0


Now it is just a matter of running ninja, which takes care of building my target

$ ninja -C out/Default/ all
ninja: Entering directory `out/Default/'
[2/2] LINK my_target


And that was it, helloworld is built.

ninja works for MacOS and Linux today, which is the combination I need, and maybe one day there will be some windows support. Since I have nothing to release yet, this is good enough for my purposes, YMMV.

Java wildcards need taming

In this year's PLDI, there is a session where every paper starts with the gerund "Taming ... "
Seems like some computer science topics are inherently wild. And what else could these papers talk about than ... Java wildcards :)

Ok, ok, it's only two papers after all. Still, the shrewishness is real, because since Java wildcards were imposed upon programmers, we find ourselves running into weird situations where people need silly casts, or declare two variables of different types for the same value "to make the compiler happy".

Well, if you feel like turning it around and make the compiler unhappy for once, try feeding it this :)

// source:
// Ross Tate, Alan Leung, Sorin Lerner.
// Taming Wildcards in Java’s Type System. in PLDI 11

import java.util.List;
class C<P extends List<? super C<D>>> implements List<P> {}
class D implements List<C<? extends List<? super C<D>>>> {}

Finishing SOLA 2011

Some pics from the SOLA run last weekend, after 11 km. I wasn't in shape at all, and for some reason was so tense that I had sore muscles in the shoulders (?) but it was good fun. I guess this is the smile of a person who is glad to be still alive :)

Prepared for SOLA 2011

Tomorrow, there is a run around Zurich, called SOLA. Teams of 14 people. Thanks to Aaron Z, I am going to take part in it. This is the first time I'll take part in a competition - excitement!

Creative Deprecation

I came across Zach Tellman's essay [1], and I find it really lucid.

quote: "There is a tension between knowledge and creation: by pursuing one, he [the technologist] retreats from the other."

Here is an essay (really, an attempt) to connect it with some things I have observed. I believe it is possible to draw a connection to what economists call Schumpeter's Creative Destruction.

Creative Deprecation

In large-scale software development it is possible to observe a large-scale pattern. One of the effects is that software engineers, while working on a development project, have to set aside some some time to learning new technologies outside of their project. This pattern consists of something like a cycle that relates knowledge about technology to creation of new technology. Here is an analogy to economy that may help clarify the scope of this pattern:

The opening up of new markets and the organizational development from the craft shop and factory to such concerns as US Steel illustrate the process of industrial mutation that incessantly revolutionizes the economic structure from within, incessantly destroying the old one, incessantly creating a new one ... [The process] must be seen in its role in the perennial gale of creative destruction; it cannot be understood on the hypothesis that there is a perennial lull.
—Joseph Schumpeter, The Process of Creative Destruction, 1942

What matters here is the system view of economy, the purported economic structure. "The" Economy is a productive chaos with too many factors to keep track of. And so is software development, we can also see it as a "system" of people learning, creating and applying technology.

The currency are artifacts of technology. Software (especially open source software) is easily accessible and usable. What is not so easily transferable is in-depth knowledge, experience about a particular piece of software technology. Every new technology (take something like Megastore [3], but also the Google Apps ecosystem), and also backward incompatible changes to technology take time to be learnt and taken up by software engineers. And integrating technology often creates something synergistic, that comes with its own characteristics.

Understanding the cycle

Let us look at the cycle. At the beginning of it, there is a team building something new that is supposed to replace something old, or change it (radically) for the better. In the middle of the cycle, people widely acknowledge that the new thing is better and it is worth investing into using it. Towards the end, people have spent enormous efforts in putting the new technology to practical use, in ways not anticipated by the initiators. As more and more people have embraced the new way, and project roll it out, shortcomings appear. In the end, the new technology has become the standard, and the old is considered something low-level or arcane.

This is very different (and sometimes conflicting) with what is usually understood under "software development cycle". The latter cycle is only concerned with a single piece of technology. This is only a small part of a larger system of creative deprecation and interacts with it.

Optimizing the cycle

The constantly changing world of available technologies and the speed at which basic assumptions are replaced by new, different ones creates friction for the software developer: it means knowledge, which had to be built up, is becoming obsolete. It means, time and resources have to devoted to learning the new stuff, even if the functional specification of the new technology is exactly the same as the old.

Software developers are humans, and as humans we have limited cognitive capacity to learn: if a technology is sufficiently complex, we cannot start using it and learn it "along the way". And here, methods exists that can help optimize the learning effect. One example of this is prototyping: we build something limited, admitting that we cannot build the whole thing at once, and the intention is to learn.

The way forward?

Claiming that this aspect has been ignored by the software industry would be going too far. There are many processes and development practices which can be understood as a concession to creative deprecation, from unit testing over javadoc to IBM's original code reviews (where developers formed committees, printed source code on paper, read it out and discuss).

The difficulty in taking advantage of creative deprecation is that our methods of "measuring" knowledge are not very developed. What are the indicators? Quality of past contributions would be a great indicator, but we don't seem to have accepted indicators for quality of artifacts either (test coverage is probably a good start).

More challenges come from the fact that individual knowledge does not add up. A team can have a wizard that wrote the book on X, and be clueless about X when that wizard is on vacation or transfers to another project. Agile methods that try to increase the "bus factor" are targeting exactly this aspect.
Preferring "simple" APIs (meaning: APIs that do not come with a high learning "price tag") is another method, trying to minimize the number of public methods are other examples.

Modest, and effective proposals are to

• acknowledge that knowledge cycle matters and be aware that reducing complexity, in the big picture, is at least as important as adding features.
• leave room for individuals to acquire knowledge, even if it is unrelated to the project
• control the cycle, by controlling time and scope of the destruction and mitigating the effects of obsoleted knowledge. For instance, alternate cycles of expansion (features, integration of new technologies) followed by contraction (optimizations, cut-over, deprecation, refactorings, bug-fixes and other maintenance) when planning a project.

[1] Becoming Eloi, becoming Morlock (wayback machine)
[2] http://en.wikipedia.org/wiki/Creative_destruction#Schumpeterian_Creative_Destruction
[3] http://highscalability.com/blog/2011/1/11/google-megastore-3-billion-writes-and-20-billion-read-transa.html

Yacc is of the Living Dead

The scientific process seems to evolve towards something like pop culture and music industry. For starters, we have publishing houses and record companies.

And then, there is a scientific article with the title "Yacc is dead" [1] which, quite possibly, has reached more people than all the accepted papers of the conference to which it was submitted.

Russ Cox criticized this paper quite harshly in an insightful blog post [2].

So, in short, the paper proposes a method that yields all parse trees and claims that the approach is "efficiently on average". The authors run a benchmark, but of course a benchmark is not exactly a proof. Russ's argument (by regexp analogy) goes something like we can make up grammars that simulate NFAs. Since there are regexps whose NFA will have O(exp(n)) possible successful runs on input of length n, (maybe something like a*a*), getting all parse trees means asking for trouble.

Where I am not so sure is, whether the authors are really unaware of this. It is possible to understand "parses efficiently on average" as "works efficiently for the average grammar programmers want to parse". Writing an ambiguous grammar by accident is one thing, writing something like a*a* is something else. Agreed, a statement like "works well for the average grammar" does not really have much scientific worth -- and Russ's criticism still stands -- but indeed it may work out in practice.

The math that derives working parsers from their specification is beautiful... the issue for practical purposes is that there are are other approaches to combinator parsing -- these are the ones that should be compared with derivative-based method, not yacc.

There is at least one paper (journal publication) out there that shows how memoization can make top-down functional parsers linear [3?], unfortunately I cannot access it so cannot comment on how applicable it is here. What's next, DMCA for papers? <b>J'accuse</b>.

Regardless what is up with yacc or memoization, among functional programming literature, there is a plethora of papers that use parser combinators to achieve polynomial parsing (the first reference that came to my mind is Swierstra and Duponcheel's paper [4]), but the wikipedia page on combinator parsing [5] has a link to more recent -- 2007 -- work from Frost and Hafiz that looks interesting.

There are no conclusions here. Combinator parsing is not new, but with the rising popularity of Scala, it is pretty much alive and kicking. After all, it has a packrat combinator parsing library included. For my next parser, I will certainly use that one and not Might and Darais approach. Still, I think the approach described in Might and Darais paper has educational value and I sincerely hope the authors will come up with a longer, more polished version.

[1] Matthew Might, David Darais. Yacc is dead.

[2] Russ Cox. Yacc is not dead.

[3?] Frost, Szydlowski. Memoizing purely functional top-down backtracking language processors. Science of Computer Programming
Volume 27, Issue 3, November 1996, Pages 263-288

[4] Swierstra, Duponcheel. Deterministic, error correcting parser combinators.  

[5] http://en.wikipedia.org/wiki/Parser_combinator

Romantic enthusiasm for verification

Recently, a workshop got me interested in contract programming again. In essence, programming by contract means we annotate our source code with pre- and postconditions.

@Requires(numChars % 2 == 0)
@Ensures(result.length() == numChars)
String foo(int numChars) {
...
}


This is like saying "the only proper way to call this method with a numChars parameter that is even. You will get a nice non-empty string in return." Sounds like a deal.

There is probably a lot to say about contracts and how they can help developers understand their code. There are frameworks that will take these annotations and turn these into run-time checks. My interest is more in verification though. Automated program verification is really hard to do, because several undecidability results apply -- but in the words of Prof Jürgen Giesl this also means that one can always improve the state of the art.

The previous time I got excited by contracts was when I had the pleasure to host Prof Peter Müller at Google where he give a talk and demo of SpecSharp. The article Specification and Verification: The Spec# Experience gives a glimpse of the programming system the authors had built. An amusing quote from there: "When programmers see our demos, they often develop a romantic enthusiasm that does not correspond to verification reality."

Let me state that dream here: a program is made of method calls. If the compiler, or IDE, "understands" the pre-conditions and post-conditions of method calls, it should be able to chain these "facts" together and achieve some form of "understanding" of the program. This can help developers add or change lines and get immediate feedback on whether the source code they write is correct.

Going back to the example above: imagine writing foo(3) in your IDE and having it underlined in squiggly red, with a mouse-over message stating "precondition numChars % 2 == 0 not satisfied".

Spec# translates the pre- and postconditions into Satisfiability Modulo Theories (SMT) problems which are then solved by the underlying engine called Boogie. Another SMT solver is Z3 which has a readable tutorial. Reading up on these, it is quite striking that Spec# is working on a real programming language, and that neat interfaces do exist between the layers of byte code, verification source and the nitty gritty predicate logic formulae.

And then, there still is the following flaw, quoted here:

At the moment you find an error, your brain may disappear because
of the Heisenberg uncertainty principle, and be replaced by a new
brain that thinks the proof is correct.
L.A. Levin

Just kidding. Robert Pollack's article is concerned with the problem that we can come up with a system that will verify our program, but we won't necessarily be able to trust it, because it is a program itself. Here is the bit that is relevant though: "My guess is that tech- 
nologies of automated proof search will be highly developed because of economic 
pressure for reliable hardware and software, and these, applied as tactics to proof 
checking, will make formal mathematics a practical reality in the foreseeable fu- 
ture."

It seems we still have a long way to go before developers see the light in IDEs having some form of automated program verification. I have a hope that if one goes back to natural deduction style proofs, logical frameworks or simple logic programming with SLD resolution, it may be possible to write reasonable (logical) annotations and have proper support. Let (expert) programmers write more. Only experimentation can show whether this is a good idea.

first baby steps with luatex

ok, I compiled the luatex beta and was puzzled on how to run this.

Then I found Luigi Scarso's answer:

what about
$texmfstart texexec --luatex luatest1.tex

What is texmfstart? No idea, but "wer sucht, der findet"

$ locate texmfstart
/usr/local/teTeX/share/texmf.local/scripts/context/ruby/texmfstart.rb
/usr/local/teTeX/share/texmf.tetex/scripts/context/ruby/texmfstart.rb

I do remember having played with context ones, but I do not remember whether I installed context there. Anyway, the .rb extension is for ruby, so

ruby /usr/local/teTeX/share/texmf.local/scripts/context/ruby/texmfstart.rb texexec --luatex sheet06.tex

did what I wanted... mostly. It produces a .pdf but it looks very basic, the page numbers are on the top of the page, and so on. Well a good starting point nevertheless.

lost in multi-lingualization

I figured out that my multi-lingual dictionary needs a multi-lingual website.

In web-design as elsewhere, i18n is quite a pain: one has to actually think what one wants before going off and doing something.

For my web dictionary and its associated websites, there is one obvious requirement: the text on every page should be viewable in various languages.

There are interesting links on the net on how to approach this systematically: I have found the following particularly useful:

• the comments in W3C's q&a blog article Content Negotiation: why it is useful, and how to make it work


• the EURESCOM report Multi-lingual web sites: Best practice guidelines and architectures

When looking for a standard encoding of languages as strings, the three letter languages codes (ISO639-2) are quite enough (ISO-639-1 are the two-letter ones). Of course, despite the thing being a standard, there is some fun to be had with e.g. deu == ger.

Apart from deciding, which languages to support, there is also a user interface question, and for my website, I consider this the most important. In times of Google, content can also be found if your website has a lousy user interface, but since I am looking for something that is fun to use interactively, usability takes priority.

That is why I need to ask myself: how would one select between languages? I think the best is to go with a hybrid approach:

• have URIs of the shape domain/language-code/path and rewrite them to domain/path.language-code.extension (the dispatching described in the comments to the W3C article).


• additionally have a footer with links (view page in language1, ..., languageN)

Pages should not be very long, so that the footer is visible. For added fun, I can later go into having facebook's wall-to-wall (two pages displayed side-by-side) layout to see the same page in two different languages, for translation and language-learning.

asp.net, and computerclubzwei

About to start a web app... coming from a Scala and Java background, but my web hoster offers me php and asp.net -- which poison is tastier? I was set to go for php, although I don't like the language much. So I thought I'd give this asp.net stuff a try.

For my first timid steps, I was happy to have read the German Wikipedia entry, and the
beginning wikibook "Webentwicklung mit ASP.NET". This had a link to visual studio web express, which is free, and it rocks as an IDE (I am a big fan of Microsoft IDEs, although I do everything to avoid owning a Windows OS). I get curious about MonoDevelop, all this Emacs juggling is getting boring sometimes.

About asp.net proper, the difference in complexity seems ridiculous compared to php... but this is more a psychological thing. While I quickly hacked a phpinfo.php to test that scripts were properly executed on the server, asp.net development first started by installing an IDE. There are quite some concepts to learn, and here I lost interest. Compared to the jsp world, the "usine à gaz" factor seems the same (I also lost interest in JSP 2, my last activity was a struts-1 webapp).

Out of curiosity, I will try to connect to the mysql database on asp.net, and continue some experiments... and if that works fine, I might stick with it and get used to IDE land again.

---

Growing up in Germany, I have at least one seen a show called "computer club" - although I was too young to appreciate it back then. Apparently, they have recently started podcasting on their new site cczwei. It's fun to listen to this professionally produced piece of audio-layman-tech-journalism - for one who enjoys people talking about technical things in a simple manner.