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

[Massimo Dentico]

Brian T Rice wrote:
> I'm sorry about not replying sooner. This needed a bit of thought, and
> I've been busy with a job...

No problem, we are all more or less busy with our lives. :-)

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

Yes, he used rewriting rules to state some equivalence (note for the
reader not familiar with Maude: it's a rewriting system).
[By the way, how is going the alpha test of the next Maude GPLed release?]

I was thinking about Joy as an example to show quotienting at work on a
programming language because it is so simple and clean syntactically and
semantically that the set of rewriting rules which discribe the language
it's also simple and small.

Moreover the conspicuous absence of variables in Joy simplify dramatically
the application of rewriting rules via unification: my memory about the
subject is very vague at the moment, but if I'm not wrong Skolemization
and occurs check (at least for first-order unification) vanish when the
target language has no variables and then unification become a simple
process of substituition. [Folk take all that with a grain of salt, please:
it comes from readings of at least 15 years ago].

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


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

This form emphasizes that y depends from x, so x is a given or in other
words is a primitive.

Now suppose in another context we have y as primitive, we can easily
derive x from the preceding equation (with aid from some rewriting rules
not shown here which assert properties of variables domain and of
operators on such domain):

    x = y - 1

Now suppose that x and y are not variables but 2 related elements
of a software system we desire to implement and also we want to port
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.

Is this rant useful for someone on this list or it just adds leading
noise? :-) [Hoping it's not simply wrong or misleading].



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

Ok, I'm glad to see that my feeble insights are in some way useful. :-)


 > > Thanks for your attention.
 >
 >
 > No problem!

Nevertheless, thanks for your replay.

-- 
Massimo Dentico