Two for the road

[Brian Rice]

At 08:52 PM 6/27/00 -0700, Lynn H. Maxson wrote:
>For a given primitive operator and associated
>operands more than one machine instruction sequence
>can produce a given (logically equivalent) result.
>Of that set at least one is equal to or greater
>than any other.  That's logic.

I'm only replying to statements which clearly lead to conclusions, which 
none of the rest of your statements have done. Please don't rant so without 
some technical proposals which are non-vacuous: simply applying to 
predicate logic without detailing the consequences or asking us questions 
about any information we may have gained is absolutely rude and sheerly 
arrogant. We've already discussed this on IRC, and you obviously have not 
listened.

>First you have to have a means of producing the set
>of logically equivalent machine instruction
>sequences.  That is not done in any existing
>compiler or interpreter.  No one reading this has
>ever experienced this occurring in any product.  No
>dialect of Lisp, for example, with its "pattern
>matching" capability has ever done this though it
>certainly lies within its capability.

If you'll read up on a system explanation I'm working on which you declined 
earlier to entertain, you'll find that we're working on that idea already 
in Slate, and it has nothing to do with the form of predicate logic (which 
is hardly uniform in the sense that Tunes abstractions must be). Predicate 
logic has scores of problems in terms of complexity, and higher-order 
predeicate logic is just horrendous as a Tunes HLL.

Just for the record, the preliminary notes on it are online at: 
http://diktuon.arrow.cx/show.php?ns=tutorial&name=User+level+types+in+Slate
which is not explicitly the same as what you propose but it has much the 
same form and can do all of the same things, while relying on the simple 
basis that the Tunes HLL guide specifies. It hasn't been clear enough to 
you, obviously, that there's a clear defining aspect of the Tunes HLL that 
you ignore: uniformity of system abstractions. This is for the sake of 
simplifying reflection; by your standards, a GNU/Linux installation is 
reflective as long as someone delivers its' Z specification with it 
(assuming one can be made). Specification in Tunes is addressed by all of 
the statements on the Tunes web site addressing formal proofs and 
verifiability, which you have not brought up. These proofs and such are to 
be delivered in the HLL itself ***without explicit bias of the language 
design towards predicate logic***! You completely fail to see our HLL idea 
as anything more than Yet Another language with the shortcomings you 
mention about Lisp, which is completely insulting.

>Now why we will accept 0, 1, or more results from a
>query and not from an optimization process is not
>clear to me.  What is clear to me is that it is
>possible.  Certainly it is a challenge.  Consider
>what it means to the cause of reflective
>programming if we meet that challenge.  One thing
>it does is reduce the user's performance risk in
>choosing a product.  It's one less thing to worry
>about.

Quit preaching to the choir. All of this is already outlined on the Tunes 
web documents, although in poor form I admit. Now start discussing real 
solutions and their details please, because you're not suggesting anything 
more than what's been demonstrated in languages that have any form of 
partial evaluation capabilities. And I seriously doubt you understand the 
range of the kinds of reflection possible. You seem narrowly focussed on 
implementational reflection, which is just one of many.

(Attempting to avoid this useless discussion as much as possible,)
~