Languages (was: Abstraction)

[Fare Rideau]

Dear Tunesmiths,
   my answer to Dave's latest post being rather long,
I've split it into several parts, by topic.

> I am more interested in the internals of the object system.  From this I
> take it that constructors and destructors is what I am talking about.  I
> want to be able to write the specification for the metalanguage in Tunes.
> This mainly includes "what is the definition of an object?" but also "how
> are objects created" and "how do they interact".
>
Ok. Great. Let's explore the subject.

First, let's explore languages and meta-languages.

A most basic concept in the mathematical theorization of computer activity,
is that of *free algebras*, *inductive types*, or equivalently *grammars*,
that are sets of *recursive structures* or *abstract syntax trees*:
given a *signature*, set of *constructors* with constraints of arity and
"type" (kinds of expressions, in the case of grammars),
we consider the set "freely generated by the construtors in this signature",
of all the terms built with those constructors and satisfying those simple
syntactic constraints.

Then, given a new such structure, we can consider functions that take
elements into the structure, and decompose them into something observable
into already known structures, which constitute accessors, or destructors.

A language is but a free algebra, that of valid source syntax trees,
as observed by a unique destructor called its evaluator.

General-purpose languages allow to define simpler free algebras,
and more elaborate destructors on them.
They are powerful enough to emulate arbitrary other languages,
though the encoding might have to be manually enforced.

A reflective system would allow to consider such sublanguages as such,
and to consistently implement them.


> You use the term "theory"-- does this mean 'object'?
>
Well, a theory is a set of meaning associated to a language;
it's a language+semantics.
It can itself be implicitly described in a meta-language,
and explicitly reified as an object in a meta-meta-language.


> The way I understand the object system, the user specifies exactly one
> object, by defining it in terms of already existing objects.

This is a combinator-based view of programming.
Note, however, that more often that not, we like to distinguish
semantic "levels", whereby objects are considered from more or
less abstract point of views. For instance, one can consider source code,
made by combining source constructs (see the theory of language grammars),
or the abstract behavior described by its evaluation, which,
if we could bypass the source-code representation, can be optimized
for execution speed.
   In a reflective system like Tunes, we like the ability to handle multiple
such semantic "levels" of programs, which do not necessarily constitute a
strict linear hierarchy of successive abstractions, but rather different
*aspects* of them programs. For instance, you'd like to have an abstract
specification of programs describing the formal problem to solve, then
add refinements corresponding to approximate formalization of informal
constraints, and, because generic problem-solving is AI-complete,
you'd like to manage more or less directly the resolving tactics used
by the system, to tune and optimize its behavior, to investigate new
strategies and correct glitches in system behavior.


> The specification consists of multiple meta-objects, each of which is a
> constraint, or statement about the object.

I would avoid the term "meta-object" here. Let's say that the specification
consists in logical constraints/statements about the object.
This means we need a framework for computational logic already.
And this framework must itself be reflectively extensible, so as to express
arbitrary new constraints, and constraints about constraints, etc.


> The statement is in terms of objects already known.
> The statements, when combined, represent the object's type.

Yes, from a logical point of view. Such type, however, is not to be confused
with the partial type information made available by traditional
"type systems" (though such type systems can be viewed as an abstract
interpretation of the full concrete type of objects).

> A function can utilize the object iff its specification
> matches or is in some way compatible with the specifications of the
> object.  In this way the statements about an object (contained in
> meta-objects) control whether an object can combine with a function.

Indeed. This is the essence of type-safety.


> How do constructors and destructors fit in with the above model?  (Mainly,
> how do constructors and destructors relate to an object's specification?)

Objects don't come out of the void. They are part of larger structures.
For instance, it's not possible to define "an integer", least you first
define the structure of the "set of integers".

Constructors are a set of operators that generate the structure in which
to build objects. For instance, the simplest definition for natural integers
is (using Coq syntax) << Inductive nat : Set := O : nat | S : nat->nat . >>:
nat is the set inductively generated by a nullary constructor O (for zero),
and a unary constructor S (for the successor of a natural number).
With constructors, you can synthetize complex terms from simpler ones.

Destructors, on the contrary, allow to analyze complex terms, reducing
them into simpler parts; they allow building not new terms, but functions
on terms, by recursing over the structure of terms. For instance,
the basic destructor generated by Coq for nat is pattern matching,
i.e. higher-order primitive recursive function generation schemes over it.
It could be given as a term of type << (T:Set)T->(nat->T)->nat->T >>:
for any type T, with an initial value for zero, and a way to find a
associated value for a number from a simpler number, you can associate
a value to all numbers. [The notion of "simpler" here gets essential
when you try to build well-founded fix points].

As said in the WWW pages, linear logic (where non-duplicable resources are
associated to objects, consumed by construction, and resumed by destruction),
happens to unify this view of constructors with the C++ "object" way.

Also, it is clear that for any type A, the notion of A-constructors
and A-destructors are A-centric: an axiomatic function of type A->B
can be considered as either a B-constructor, or as an A-destructor,
depending on the point of view. If you tend to neglect A (for instance,
A being an implicit element of an almost infinite store), then you'll
naturally say it's a B-constructor. If you tend to neglect B (for instance,
you giving back memory to the infinite store), then you'll naturally it's
an A-constructor.


> Here is what I understand of variants and invariants:  The invariant is
> the object specification, and doesn't change.
Right. If the invariant changes, then it's no more the same object
(though it may be a new incarnation of the same project).


> Variant is anything dynamic, like implementation detail or current
> detected range of a value

In my own view, I use the term for a well-founded magnitude that must
decrease during execution, until it eventually reaches some fixed point,
which is considered a "better" state.
For instance, when executing a recursive function, the complexity
of the unexplored part of objects will decrease until the function is
completed, yielding a result. When you're optimizing a program,
the slowness of the program will decrease until it's optimal (according
to the "optimizer"'s criterion).

Well, I admit the notion of variant is less clear than that of invariant;
actually, I've never seen it discussed in the classic literature.
I wanted that it be possible to internalize into the system the formal or
informal notions of "cost", of "efficiency", etc, so that reflective
cost-analysis and optimization be possible from inside the system,
consistently with guaranteeing of invariants. So that it be possible
to define several tactics, and let the system choose between them,
not according to just a blind strategy, but to a cost-aware one.

The system's responsibility is not just to enforce the invariants,
but also to reduce the variants. Of course, the system can give
formal guarantees with respect to variants and invariants only
in as much as formal specifications and proofs/strategies where given to it.


> Is function application a constructor because it returns an object?

Function application is definitely a syntactical constructor of programs.
It may also be an operation, in a operational semantics for programs.
But if you abstract away the syntax and use some kind of denotational
semantics, then there are no more function applications.
It all depends on the aspect you choose for programs.


> Are functions then also destructors because they make use of objects?

Well, while "constructor" and "destructor" is a syntactical notion,
it is sometimes useful to consider the same abstract programs
as expressed using a different syntactic frameworks, so as to
interrelate properties of them that are easier to prove in either framework.
So, every function can be definitely be considered to destruct(urate) objects
given as parameters, and/or to construct objects given back as results,
by adding it as a new constructor/destructor axiom to an enriched or modified
language. Depending on which functions are atomic constructors/destructors,
and which are complex combinations thereof, different aspects of programming
are revealed, different theorems/programs are made easy to prove/construct.


For instance, the classical way to define A-lists in Coq is as
Inductive list : Set := nil : list | cons : A->list->list.

But you could as well define them as
Inductive non_empty_list := atom : A -> non_empty_list
	| append : non_empty_list->non_empty_list->non_empty_list .
Inductive list := nil : list | non_nil : non_empty_list -> list .
You'd have to quotient non_empty_list modulo associativity of append.

Lots of theorems are made much simpler with append and associativity
being axiomatic constructors instead of functions. Of course, you have to
prove the isomorphism between your two definitions for lists; but once
you're done, then you get lots of things for free, as you can freely
go from one aspect to the other.


> I was mistaken about the use of lambda.  I thought "basic constructors"
> meant the fundamentals of the object system.  I am trying to establish a
> complete picture of the tunes metalanguage, the part of the system that is
> syntax-less.

Beware that we're never syntax-LESS, but rather syntax-INDEPENDENT,
which is different: I could equivalently explain my ideas in french,
or in another language (should I know one well enough), but still,
I do need a language in which to explain my ideas. The same goes with
computer programs, in Tunes or whatever system. We cannot get rid of
having program representations for the user to read and write
(though such representations need not be streams of characters, either).
However, we can establish mutual translations between those representations,
and choose representations that are better suited than others to some set
of manipulations of another.


> If the expression is not syntactic, but already internally represented, as
> an expression tree, what is abstraction then?
>
Expression trees are themselves but a more abstract view on syntax:
instead of having a flat character stream representation of program text,
with a requirement on implicit program structurability, trees show explicit
program structure. Trees are still essentially syntactic: their full name
in this context is "Abstract Syntax Trees", after all.

Abstraction is still the syntactical ability to deduce
the syntax of a function from a pattern of abstract arguments,
and the syntax of a body. Function application of an abstraction
matches the concrete parameters to the argument pattern, and consequently
substitutes matched values to abstract arguments in the function body,
before to evaluate it.


== Faré -=- (FR) François-René Rideau -=- (VN) Уng-Vû Bân -=- rideau@ens.fr ==
Join a project for a free reflective computing system! | 6 rue Augustin Thierry
TUNES is a Useful, Not Expedient System.               | 75019 PARIS     FRANCE
http://www.eleves.ens.fr:8080/home/rideau/Tunes/ -=- Reflection&Cybernethics ==