[TYPES] rewriting of typed combinator expressions

[Matthias Felleisen]

On Aug 4, 2004, at 6:17 AM, Thorsten Altenkirch wrote:

> I believe that one-step reduction is a bit of a historical mistake: 
> who executes their programs by
> rewriting them to normal forms (maybe mathematicans)? More realistic 
> is to define a big-step semantics which
> can be easily turned into a functional program which can be further 
> turned into a machine (by making it tail
> recursive) .

While this has nothing to do with the original question, I need to 
reply to this statement. It is of course extremely natural to have a 
one-step relation that reduces programs one step at a time, until the 
program is in a certain shape. This is exactly what the machine does, 
and it is therefore appropriate to call this form of semantics an 
abstract, text-based machine (as I have done for 20 years now).

What is wrong is to reduce to normal form. Programs (statements and 
expressions) are never evaluated to normal form on any realistic 
machine; the machines stop when it reaches a "value" i.e., something 
that we all agree is a final answer. Examples are numbers, booleans, 
and I'd hope closures. The body of the closure can be an arbitrary 
term.

As for the choice between a big-step semantics (as you call it) and a 
one-step reduction semantics, you should probably understand that it 
all depends on (1) the purpose of your model (why do you make a model 
of a programming language) and (2) what's in your programming language. 
For example, I studied the addition of assignment and continuations to 
a plain functional core in the 80s. I can design whatever form of 
semantics you want. But, after checking out a number of different 
scenarios, I find that I almost always want a semantics based on 
one-step semantics. It's at least as natural (sorry) and as useful as a 
big-step semantics in almost all non-trivial (i.e., purely functional) 
cases.

-- Matthias