[TYPES] rewriting of typed combinator expressions

[Matthias Felleisen]

On Aug 4, 2004, at 10:51 AM, Thorsten Altenkirch wrote:

>
>
> 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):

But why would I even start with the premise of wanting to write an 
interpreter? That's just another way of saying "I want big-step 
semantics, because I want big-step semantics." You made a general claim 
about one-step semantics. I dispute that, and I am saying that in many 
situations, a one-step semantics is a better choice than a big-step = 
interpreter semantics.

-- Matthias