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

[Joerg F. Wittenberger]

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"

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

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

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

> To clarify what we are speaking about, an example (WARNING: this is an
> etremely trivial example and its purpose is to give just a flavor to grasp
> superficially the concept). Suppose we have such a simple equation:
> 
>     y = x + 1
[...]
> our software on (at least) 2 different platforms: on a platform P1
> is more simple/efficient to map x onto available CPU instruction
> set/OS API/library interface and derive y. Instead on another platform
> P2 is more simple to map y and derive x.
> 
> 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.

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.

> > > (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?

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.

Best regards

/Jörg
-- 
The worst of harm may often result from the best of intentions.