[TYPES] rewriting of typed combinator expressions

[Thorsten Altenkirch]

Matthias Felleisen wrote:
> 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).

If somebody asks me (or you) to write an interpreter for a functional programming
language, I suspect we both would come up with something like (obviously your
versions would have more brackets):

data Tm = Var String | App Tm Tm | Lam (String,Tm)

data Val = VClos (String,Tm) Env

type Env = [(String,Val)]

eval :: Env -> Tm -> Val
eval e (Var x) = v
     where Just v = lookup x e
eval e (App t u) = eval ((x,v):e') t'
     where VClos (x,t') e' = eval e t
           v = eval e u
eval e (Lam xt) = VClos xt e

We would not look for a redex reduce it and then apply the same procedure to
the term obtain by replacing redex by reduct. Hence, I do not see why one-step
reduction is "extremely natural".

> 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.

First of all there is no doubt that I appreciate your contributions to the
area. However, I do believe that the best way to understand computational
effects is by using a monadic, i.e. semantic explanations, of what effects
mean. It seems to me that concentrating on syntax and small step reductions
it is hard to see the big picture.

Cheers,
Thorsten


-- 
Dr. Thorsten Altenkirch		   phone : (+44) (0)115 84 66516
Lecturer			   http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT	   University of Nottingham

This message has been scanned but we cannot guarantee that it and any
attachments are free from viruses or other damaging content: you are
advised to perform your own checks.  Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.