Short note on "quotienting" (was: Comments requested)

[Brian T Rice]

I'm sorry about not replying sooner. This needed a bit of thought, and
I've been busy with a job...

On Sat, 14 Dec 2002, Massimo Dentico wrote:

> Brian T Rice wrote:
> > So I presume there are no objections or strong opinions either way...
> >
>
> Hello Brian,
>
> I'm slowly reading yours update.
>
> IMHO an important concept/term as "quotienting" (HLL Principles/
> Extensibility/Quotienting) needs a better/more broad explaination
> for people without a solid mathematical background (like me).

Absolutely.

> In particular how this principle enables a no-primitives/no-kernel (1)
> system and how is pertinent even for (meta-)translation (morphism:
> by the way, when is it more appropriate/correct to use quotienting
> and when morphism? The explaination speaks about isomorphism, so
> quotienting is a particular case of morphism?)

Yes, quotienting is the use of a(n iso-)morphism to translate some data in
a reflective kind of way. So quotation of code is a limited example, but
so is mirror-style reflection.

> Some work on Joy, by Brent Kerby (Iepos) could be showed as not so
> bad example of (in the sense that at the time he was not working
> to illustrate) this principle in act: he chooses a set of combinators
> and derives the rest, there isn't such thing as a primitive in
> absolute sense (well, of course there is where the hardware begins).

This is somewhat the case. A full demonstration of the idea would be a
Joy system where the choice of what is primitive and what is derived is
totally transparent to the user at run-time. This means that effectively
no functions are defined in terms of other functions, at a certain level,
or at least within a certain region of the system. A further demonstration
would have these different bases for combinator-functions existing
side-by-side at run-time, with the ability to shift between bases for,
say, efficiency's sake.

One of the reasons that I like Maude is that it's much closer to being
able to express this.

> All this probably is also related to what you (or Far=E9) have written
> in Interfaces Subproject: "In contrast to these approaches, the Tunes
> principle of interfaces is to standardize on media which are logical
> or algebraic and still capable of expressing low-level types as needed."
> In fact a programming language is a particular kind of medium for
> human-computer interaction.

I modified a statement of Fare's to produce that, so it's a combination of
our ideas. It is definitely describing a use of quotienting, anyway.

> Last but not least I see some connections with what is called physical
> and logical indipendence in the data base field, the motivation number
> one for the relational data model (and that AP5 support better than
> current SQL DBMS).

Absolutely. And AP5 is such a good example for it.

> What do you think about my comprehension of the matter? I'm not
> sending this mail to the list because if I'm misunderstandig
> some (or all) important aspect and these are all nonsense I could
> confuse other people.

It's pretty good. Obviously there needs to be a specific area of the
semantics description that addresses this very important point. It's a
different kind of application of the rewrite semantics than is described
in the Rewrite section, so that is probably what will be extended.

> Thanks for your attention.

No problem!

> Notes
>
> (1) No-kernel has 2 important aspects: no overhead for protection,
>      but security through proofs/capability, and no-API, the aspect
>      relevant in this context.

That's a good connection to bring up. I'll try to fit that in.

--=20
Brian T. Rice
LOGOS Research and Development
mailto:water@tunes.org
http://tunes.org/~water/