notes-computer-programming-programmingLanguageDesign-prosAndCons-structuralOperationalSemantics

http://existentialtype.wordpress.com/2011/03/21/the-dog-that-didnt-bark/ argues that the right way to teach induction and recursion is to use a language with Plotkin’s structural operational semantics, and then to explain recursion in terms of reductions, not in terms of a call stack:

" What makes structural operational semantics so useful is that the execution model is directly defined by an inductive definition of a transition relation, M\mapsto M', on programs. (I don’t have the space to explain it fully here, but you may consult Practical Foundations for Programming Languages for a full account.) The crucial idea is to use inference rules to give a structural definition of evaluation for programs themselves, not a translation into some underlying abstract machine code. For example, one rule for evaluation of addition expressions is

    \displaystyle{M\mapsto M'\over M+N\mapsto M'+N},

Another rule states that

    \displaystyle{N\mapsto N'\over m+N\mapsto m+N'},

where $m$ is a number, and a third states that \displaystyle{m+n\mapsto p}, where $p$ is the sum of $m$ and $n$. With these (and similar) rules in place, one may give an execution trace in the form

    M_1\mapsto M_2 \mapsto \cdots \mapsto M_k,

which makes explicit the steps of evaluation. Each step is justified by a “proof tree” consisting of a composition of rules. Importantly, the size of the expressions M_i correlates directly with the space required by an implementation, allowing for a clean and clear explanation of space issues such as tail recursion.

This is a good start for explaining the semantics of a recursive function, but the real beauty of type theory emerges when teaching how to reason about a recursively defined function. The lesson of type theory is that induction and recursion are the same thing: an inductive proof is a recursive function, and a recursive function is an inductive proof. This means that there is really only one concept here, and not two, and that the two go hand-in-hand. ... Perhaps the most important thing, though, is to convey the sense of inevitability and naturality about induction and recursion. Don’t talk about proof as a separate topic! Don’t operationalize recursion beyond the bounds of the language model. "