🚀 go-pugleaf

In article <5504@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) writes:
>
>It seems more important, for the sake of referential transparency,
>that denotational equality should imply operational equality.
>(Is this what is meant by "adequacy" of the model?)

Yes, this is the "adequacy" of the model which has to hold if the
denotation should make any sense at all.

>
>However, I don't forsee anybody complaining,
>"I compared the execution of two programs on all possible inputs,
>and though my denotational semantics says the programs are not the same,
>after watching both for all eternity I noticed that
>both results are equally undefined on everything I tried!"
>
>The notion of operational equality seems incomplete to me,
>because you _cannot_ compare their behavior on all possible inputs
>if some of those inputs cannot be expressed in the language.

Operational equality is not defined as "equal on all inputs". If two
parts of the programs are observationally not different in all
contexts of the language, then they are operationally equivalent. To
prove this you don't need to run the programs. You can prove things
based on reduction rules etc. Often this is painful, as you have to
use induction on length of the reduction or some such equally
difficult proof method. In fact, when I said that F_1 and F_2 are
equal operationally, I can prove it using the reduction semantics(i.e.
they are equal in all contexts). I find it somewhat difficult to
follow that is one of the reasons why I prefer proofs using
denotational semantics.

What is disturbing is when I prove that two functions are not equal,
some theory based on reduction semantics tells me that they are equal.
Then the full power of denotational semantics is lost.
>
>My question was,
>"Since our language is not going to be fully abstract anyway
>(due to lack of provision for defining parallel functions),
>what _further_ loss results from replacement of a strict-cons
>by a lazy cons accessed from within a strict function
>(so that arguments are verified as being above bottom
>before application of the lazy cons)?
>
>Frank Silbermann	fs@cs.tulane.edu
>Tulane University	New Orleans, Louisianna  USA

I misunderstood your question last time. Sorry about that.

It seems to me that more and more inequalities that hold in the model
won't be true in the language (i.e. there is no further "qualitative
loss"). For me it is a sure sign that either I am modeling the
language wrong, or the language needs to be fixed. I believe that the
continuous model is not suitable for a sequential language.

-- rama