axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Axiom musings...


From: Tim Daly
Subject: Re: Axiom musings...
Date: Tue, 10 Nov 2020 02:14:24 -0500

Another area that is taking a great deal of time and effort
is choosing a code architecture that has a solid background
in research.

Axiom used CLU and Group Theory as two scaffolds to
guide design choices, making it possible to argue whether
and where a domain should be structured and where it
should occur in the system.

Axiom uses a Pratt-parser scheme. This allows the
ability to define and change syntax by playing with the
LED and NUD numeric values. It works but it is not
very clear or easy to maintain.

An alternative under consideration is Hutton and Meijer's
Monadic Parser Combinators. This constructs parser
functions and combines them in higher order functions.
It is strongly typed. It provides a hierarchy of functions
that would allow the parser to be abstracted at many
levels, making explanations clearer.

Ideally the structure of the new parser should be clear,
easy to maintain, and robust under changes. Since SANE
is a research effort, maximum flexibility is ideal.

Since SANE is intended to be easily maintained, it is
important that the compiler / interpreter structure be
clear and consistent. This is especially important as
questions of which proof language syntax and a
specification language syntax is not yet decided.

Tim




On 10/9/20, Tim Daly <axiomcas@gmail.com> wrote:
> A great deal of thought has gone into the representation
> of functions in the SANE version.
>
> It is important that a function lives within an environment.
> There are no "stand alone" functions. Given a function
> its environment contains the representation which itself
> is a function type with accessor functions. Wrapped
> around these is the domain type containing other
> functions. The domain type lives within several
> preorders of environments, some dictated by the
> structure of group theory, some dictated by the structure
> of the logic.
>
> Lisp has the ability to construct arbitrary structures
> which can be nested or non-nested, and even potentially
> circular.
>
> Even more interesting is that these structures can be
> "self modified" so that one could have a domain (e.g.
> genetic algorithms) that self-adapt, based on input.
> Or "AI" domains, representated as weight matrices,
> that self-adapt to input by changing weights.
>
> Ultimately the goal of the representation should be that,
> given a function, it should be possible to traverse the
> whole of the environment using a small, well-defined
> set of well-typed structure walkers.
>
> All of this is easy to write down in Lisp.
> The puzzle is how to reflect these ideas in Spad.
>
> Currently the compiler translates all of the Spad
> code to Lisp objects so the Spad->Lisp conversion
> is easy. Lisp->Spad is also easy for things that have
> a surface representation in Spad. But, in general,
> Lisp->Spad is only a partial function, and somewhat
> limited at that.
>
> I suspect that the solution will allow some domains
> to be pure Lisp and others will allow in-line Lisp.
>
> Most of these ideas are nearly impossible to even
> think about in other languages or, if attempted,
> fall afoul of Greenspun's Tenth Rule, to wit:
>
>   "Any sufficiently complicated C or Fortran program
>    contains an ad hoc, informally-specified, bug-ridden,
>    slow implementation of half of Common Lisp."
>
> Fortunately Spad is only a domain specific language
> on top of Lisp. Once past the syntax level it is Lisp
> all the way down.
>
> Tim
>



reply via email to

[Prev in Thread] Current Thread [Next in Thread]