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

[Brian T Rice]

On Sat, 15 Mar 2003, Joerg F. Wittenberger wrote:

> Hi all,
>
> > It is often found in theoretical textbooks in maths or CS that "it
> > does not matter which (terms) are primitive and which are derived",
>
> ok.  though I like the term "axiom" better for "primitive"

Or "axiomatic".

> > which is a particular case of the principle according to which
> > objects are to be considered "up to isomorphism".
>
> Bang.  I didn't get that at all.  What do you want to express with "up
> to isomorphism".

That anything that /behaves/ identically regardless of its implementation
expresion, should be usable by a programmer identically. The phrase you're
quoting is mathematically- or logically-oriented in that it appears in a
lot of textbooks because of their emphasis on the idea of an isomorphism:
a 1-to-1 mapping between objects in domains.

> > Among the basic constructs of the language, there must be some way
> > to quotient a structure by any given equivalence relation on that
> > structure, and keep whatever operations on this structure with which
> > the equivalence relation is compatible.
>
> I do have the strange feeling that I know "to quotient" as "to quote"
> from the LISP speaking.  Is this understanding correct?

Lisp's <quote> operator is a very primitive implementation of quotienting.
Basically quotienting is any abstraction where you take a class of things
according to some set of rules and provide new identities for objects that
behave identically. For example, if you want to describe the Rational
numbers while knowing only the Integers, you can describe:

"answers to the equation a * x = b for all Integers a and b"

as describing quotients of Integers (this is where the term comes from).
The Rationals then are described as a domain of new (derived) objects,
each of which is the set of equations which describe some equivalent or
isomorphic concept. For example, the object we call "5/3" is an
equivalence class of equations such as x * 3 = 5, x * 6 = 10, and so
forth. So the quotienting is happening on pairs of Integers with this
equation, (3,5) , (6,10) , (21,35), etc. This is generally part of the
mathematical tradition of forming inductive definitions from primitive
axioms to describe higher-level concepts, but the point with Tunes is that
we don't care which parts are core and derived: we want to be able to
implement some concept and translate back and forth across an isomorphism
as we need to. We deliberately do not want to care about implementation
decisions after they are made.

Thanks for bringing this up; I will add an explanation based on this to
the CLiki and link to it from the documentation on the main site.

> > Of course Joy, as is now, doesn't have such feature (quotienting),
> > much less at run-time (but I guess it's less difficult to add quotienting
> > in Joy than in other system, indeed in virtue of quotation and the absence
> > of variables).
>
> Though I also don't really know what variables where good for, I have
> to admit that I don't kow anything about Joy.  And my day job won't
> permit getting that any time soon.  Short examples would be welcome.

I think the only example for Joy is that code and lists are treated
somewhat identically, since in Joy code has this shape. I wouldn't read
too much into that.

[snipped an example]
> > In the first case, P1, we have x as primitive, in the second y instead.
> > With quotienting we can obtain such flexibility in choosing what is
> > primitive and what is derived.
>
> Hm.  Apparently I'm wrong in the understanding of "quotienting" as
> "quoting" above.  But here I would feel that some kind of
> bidirectional equivalence function together with some caching would
> do.

Yes, that's an isomorphism. The arrow framework I want to build would
include a kind of caching system; actually it does already but is not
sufficiently sophisticated yet for Tunes. In general there are a network
of types and isomorphisms, so the problem is roughly analogous to routing
on the Internet (perhaps I am stretching a metaphor a bit too far, but it
works for now). ;)

> Both taken together would mean: the system needs to have a notation of
> structures which can express functions and protocols.  It needs to be
> able to derive tranformations rules to convert between functions or
> protocols from the basic notation and choose the best according to the
> context (e.g., the hardware/software it is running on) transparentely
> to the user.

Yes, that is a decent summary. The details are a bit more hairy, of
course.

> > > > (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.
>
> no-API?  Hm.  So what are the abstraction barriers the system build on
> downwards and provides upwards?  Or better say, how do you call them,
> if not API?

They are Interfaces without the static notion of Application and
Programmer to get in the way. If you use a capability-style concept of
security (see http://cliki.tunes.org/Capability), then you can see that
access to functionality can be given in an incremental fashion: just as
much as is needed or perceived as generally appropriate, and not more
without some kind of contract or at least some reasoning. One of the E
authors gives an example where an Outlook worm has to ask the user several
questions explicitly before it can propagate: "Can I read your address
book?" "Can I resend to all of them?" and such. Such a model can be
configured to keep these nasty annoyances of the current user-permissions
system from becoming as rampant as they are.

> If there are none at all, the system would encompass everything, which
> means just as much as nothing.  It wouldn't be useful at all.

Oh, that's a little too broad a brush you're painting with. The system
would be able to publish interfaces (APIs) within itself, so it's not as
bleak and nihilistic as it sounds.

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