Re: Term Rewriting vs. Functional Programming

Vesa Karvonen <vesa.karvonen@xxxxxxxxxxxxxx> writes:

> Matthias Blume <find@xxxxxxxxxxxxxxxxxxxx> wrote:
>> Vesa Karvonen <vesa.karvonen@xxxxxxxxxxxxxx> writes:
>
>> > Matthias Blume <find@xxxxxxxxxxxxxxxxxxxx> wrote:
>> >> Vesa Karvonen <vesa.karvonen@xxxxxxxxxxxxxx> writes:
>> >
>> >> My point (and Andreas' point) was that the ML definition simply does
>> >> not extend into this territory at all. Reasonable implementations, of
>> >> course, will eliminate tail calls (i.e., implement them as jumps).
>> >
>> > Perhaps our views on this matter are different, but thinking about it, I
>> > definitely prefer reasoning about my programs based on semi-formal
>> > requirements in a definition than based on what is or isn't a "Reasonable
>> > implementation".
>
>> But you can't "reason" about your programs in the strict sense of the
>> word with only semi-formal (and, more importantly, incomplete)
>> requirements.
>
> I would definitely like to know whether a server loop written in SML will
> run in constant space or not.

So do I. But to be able to know that, it is not enough to know that
the compiler optimizes tail calls.

> An argument based on "reasonable
> implementation" seems totally unsound to me,

Right. But you are arguing for such an argument by asking for an
incomplete "semi-formal" specification.

> but an argument based on a
> formal syntactic definition of tail calls and an informal definition of
> what tail call elimination means seems quite reasonable to me.

But it isn't. To know that your server loop runs in constant space,
you need to know a whole lot more about how your compiler handles the
rest of the language in terms of space usage.

>> You are supplementing the written requirements with your own
>> implementation model. In fact, such a model is necessary to even make
>> sense of the "tail call" requirement.
>
> You mentioned discussions on comp.lang.scheme. I've just spent quite
> a bit of time browsing through some discussions and it seems like the two
> sides are
> - compiler writers (e.g. Siskind of Stalin fame) who have difficulties
> translating Scheme efficiently to C [;-)] and, for some reason, want to
> complicate the notion, and
> - people (too many to mention) who want to write programs in Scheme, are
> quite happy with a simple syntactic definition of tail calls, and want
> reason about the space usage of their programs.

That's not the kind of discussion I meant. There is a third (small)
group of people which includes myself that says:

- Don't specify unless you specify completely enough so that the
specification has meaning.

> I couldn't find any definitive conclusion. If you have a specific
> discussion in mind, I'd like to see a pointer to it. Based on what I saw,
> it seems that syntactic definition of tail calls is a reasonable approach.
> IOW, I couldn't see a convincing argument as to why it would be
> unacceptable.

It is not unacceptable. But it is only a tiny part of the whole
picture, and by far not enough to provide a basis for the kind of
reasoning that you evidently try to use.

> If the issue is that you need to specify an upper bound on the space usage
> of "everything", then I don't see why that would be a show stopper.

It is not a show-stopper and has been done. My point is that you have
to do it. Simply saying "optimize tail calls" while leaving out the
(far bigger) rest is not enough.

Do it right, or don't do it at all.

Matthias
.