Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!rex!fs
From: fs@rex.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.functional
Subject: Re: Intermediate Codes for Functional Languages
Message-ID: <5513@rex.cs.tulane.edu>
Date: 21 Dec 90 19:53:03 GMT
References: <1990Dec20.190014.20982@rice.edu> <5504@rex.cs.tulane.edu> <1990Dec20.215506.25243@rice.edu>
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 56

In article <1990Dec20.215506.25243@rice.edu> rama@tone.rice.edu (Ramarao Kanneganti) writes:
>
>	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.
>	I find it somewhat difficult to follow; that is one of the reasons
>	why I prefer proofs using denotational semantics.

Indeed.  I thought the whole purpose of declarative programming
is that we can reason about programs in the _semantic_ realm.
We want to use mathematics to prove things about our programs,
not vice-versa.

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

This just says that operational "equivalence" is weaker than true equality
(yet another reason to prove things via the model, not the syntax).

>	It seems to me that more and more inequalities that hold
>	in the model won't be true in the language.

You mean, won't be _observable_ in the language.
The solution is to stop identifying operational equivalence
with equality.

>	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

I don't think it's as bad as all that.
Even in arithmetic, we model our language via
the _real_ numbers, even though we probably cannot denote
every one of them in our notation.
Why do we put up with this in mathematics
(having models which are richer than the language)?
Probably because sometimes a stronger result
(e.g. a theorem about the model)
is easier to obtain than a weaker result
(e.g. a theorem about the language).

In the functional programming field,
I would like to see fewer papers about lambda calculi,
and more papers about domain models for functional languages,
especially the polymorphicly-typed kind.
(I'd write one, myself, if I could figure out how :-)	).

	Frank Silbermann	fs@cs.tulane.edu
	Tulane University	New Orleans, Louisianna  USA