Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings

[Tim Daly]

>"Curried functions may be used in any programming language that supports 
>closures;
>however, uncurried functions are generally preferred for efficiency reasons, 
>since the
>overhead of partial application and closure creation can then be avoided for 
>most function
>calls."See also the paragraph on "Contrast with partial function application."

Overhead of creating a curried lisp function is almost nothing. Lisp
handles closures
and function creation all the time. A macro to create a curried lisp
function is a small
classroom exercise.

>Moreover, under the paragraph on "Category theory,"

>"Currying can break down in one of two ways. One is if a category is not 
>closed, and
>thus lacks an internal hom functor (possibly because there is more than one 
>choice
>for such a functor). Another ways is if it is not monoidal, and thus lacks a 
>product
>(that is, lacks a way of writing down pairs of objects). Categories that do 
>have both
>products and internal homs are exactly the closed monoidal categories."

Indeed. I suspect, though I don't know, that most of the Axiom functions based
on group theory are closed monoidial. The same is likely true tor the data
structure manipulating code.

>The rest of that paragraph is also worth reading and by examples, it shows
>perhaps why the logic notation is preferred because closed monoidal categories
>are very common.

>"By contrast, the product for monoidal categories (such as Hilbert space and 
>the
>vector spaces of functional analysis) is the tensor product. The internal 
>language
>of such categories is linear logic, a form of quantum logic; the corresponding 
>type
>system is the linear type system.

Frank Pfenning http://www.cs.cmu.edu/~fp/
taught me everything I know about linear logic. He has pointed
me at papers and talks (especially his Oregon lectures,
https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php
as well as Stephanie Balzer's lectures). I admit I do not yet have a handle
on where I can use linear logic. It applies really well in communication but
I'm not sure how to apply it in the Axiom context, except in the conext of
parallel computation. However, I'm still climbing the (near-vertically) steep
hill of logic and proofs. The amount I don't know currently fills 3
shelves of my
bookcase.

>Even if the goal is to have compatibility with other systems that uses currying
>or logic convention, it may not make sense to change the Axiom signature
>syntax for multi-input functions (which requires changes to the compiler and
>other components).

I am rewriting the compiler / interpreter in Common Lisp CLOS. CLOS can
handle most of Axiom's inheritance automatically. I have most of the categories
built so far. For non-standard lookups it provides an override.

Since the new (Sane) compiler is going to handle logic syntax for axioms,
theorems, and specification it seems reasonable to use a syntax and semantics
from the existing proof systems (Coq, Lean, etc..). I will have to export proofs
to those systems both because they need to trust Axiom (I hope Axiom can be
the "Oracle" for proof systems doing computation) and because I'm not
smart enough to do otherwise.

>Perhaps a compromise would be to create a bidirectional
>translation Axiom package to facilitate the interfaces (that is, an 
>implementation
>of currying and uncurrying in Axiom to the targeted CAS using the currying
>convention). This should not be too hard in Lisp (for you :-)). This has the
>advantage that if the computation is from a currying system but to be done
>in Axiom, there is only one overhead call (uncurrying) for input, and perhaps
>another for output (currying, if the output is a function type); and if the
>computation is from Axiom but to be done in a currying system, there is
>also just one overhead call (currying) for input (here, I assume the currying
>system has optimized its implementation), and perhaps another (decurrying,
>if the output is a function).

Currying isn't really that much of a motivation for adopting logic syntax.

The main reason is that most people in computer science these days are
generating papers using rules and judgements (witness the talk given at
CCNY by Andre Platzer combining logic and differential equations).
https://www.youtube.com/watch?v=4QDeZnw7_m0

Guy Steele gave a talk where he counted the use of logical notation trends
in published research papers. It is now well above 50 percent.
https://www.youtube.com/watch?v=dCuZkaaou0Q

I could easily accept both Axiom's input forms and Logic input forms
but the world seems to use the logic forms, even in code (e.g. Haskell).
Given that about a dozen people use the Axiom notation why would it
make sense to use it for Spad and a different notation for the axioms?

Axiom's syntax is really showing its age.

The more interesting (and not in a good way) change is my current
struggle over using unicode in the input/output syntax. Should the 'sum'
function be 'sum' or '\sum' (i.e. a sigma)? Is subscript I/O unicode?
Can you write an integral sign in a signature as a function name?

The unicode issue is further highlighted by the fact that X11 support
is going into "maintenance mode". That means I have to move the
documentation and graphics to a browser or jupiter front-end. I have
previously worked out the Axiom browser notebook (Volume 11) but
not the graphics.
https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)

More interesting is the issue of moving from the 1960s CHARYBDIS
I/O to in-browser latex I/O. The output equations are much prettier.
And the current trend for input seems to be a form of in-browser
literate programs, witness:
https://leanprover.github.io/tutorial/
and
https://x80.org/rhino-coq/

>There is no need to reinvent the wheel for either system

Axiom is an amazing collection of algorithms but it is not keeping
up with current trends. Nobody wants to work in a system that will
die of old age so we need to adapt and grow. "More of the same"
is not enough. By combining computer algebra and proof systems
with a more current front end and better literate documentation
we are breaking new ground, which should keep us relevant for at
least a few weeks at the current world speed.

I thought "The 30 Year Horizon" was further away...

Tim







On 7/12/19, William Sit <address@hidden> wrote:
> Dear Tim:
>
> According to Wiki on currying (https://en.wikipedia.org/wiki/Currying,
> paragraph on lambda calculi):
>
> "Curried functions may be used in any programming language that supports
> closures; however, uncurried functions are generally preferred for
> efficiency reasons, since the overhead of partial application and closure
> creation can then be avoided for most function calls."
> See also the paragraph on "Contrast with partial function application."
>
> Moreover, under the paragraph on "Category theory,"
>
> "Currying can break down in one of two ways. One is if a category is not
> closed, and thus lacks an internal hom functor (possibly because there is
> more than one choice for such a functor). Another ways is if it is not
> monoidal, and thus lacks a product (that is, lacks a way of writing down
> pairs of objects). Categories that do have both products and internal homs
> are exactly the closed monoidal categories."
>
> The rest of that paragraph is also worth reading and by examples, it shows
> perhaps why the logic notation is preferred because closed monoidal
> categories are very common. In particular:
>
> "By contrast, the product for monoidal categories (such as Hilbert space and
> the vector spaces of functional analysis) is the tensor product. The
> internal language of such categories is linear logic, a form of quantum
> logic; the corresponding type system is the linear type system. Such
> categories are suitable for describing entangled quantum states, and, more
> generally, allow a vast generalization of the Curry–Howard correspondence to
> quantum mechanics, to cobordisms in algebraic topology, and to string
> theory.[1] The linear type system, and linear logic are useful for
> describing synchronization primitives, such as mutual exclusion locks, and
> the operation of vending machines."
>
> Even if the goal is to have compatibility with other systems that uses
> currying or logic convention, it may not make sense to change the Axiom
> signature syntax for multi-input functions (which requires changes to the
> compiler and other components). Perhaps a compromise would be to create a
> bidirectional translation Axiom package to facilitate the interfaces (that
> is, an implementation of currying and uncurrying in Axiom to the targeted
> CAS using the currying convention). This should not be too hard in Lisp (for
> you :-)). This has the advantage that if the computation is from a currying
> system but to be done in Axiom, there is only one overhead call (uncurrying)
> for input, and perhaps another for output (currying, if the output is a
> function type); and if the computation is from Axiom but to be done in a
> currying system, there is also just one overhead call (currying) for input
> (here, I assume the currying system has optimized its implementation), and
> perhaps another (decurrying, if the output is a function).
>
> There is no need to reinvent the wheel for either system.
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> ________________________________________
> From: Axiom-developer
> <axiom-developer-bounces+wyscc=address@hidden> on behalf of
> Tim Daly <address@hidden>
> Sent: Friday, July 12, 2019 5:11 AM
> To: axiom-dev
> Subject: Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings
>
> Temptation...
>
> I would like to remain faithful to Axiom's syntax for signatures
>
> foo: (%,%) -> %
>
> but the world seems to have converged on
>
> foo: % -> % -> %
>
> This shows up everywhere in logic, in haskell, etc.
> It allows for a primitive kind of currying, the "right curry"
> (Some form of scheme allows currying anywhere in the
> argument list, including multiple currying)
>
> I need to logic-style signatures for the axioms so the
> tempation is to rewrite the Axiom signatures using the
> logic notation.
>
> I can do both but it might be clearer to follow the world
> rather than follow our own, given the user base.
>
> Tim
>
>
> On 7/9/19, Tim Daly <address@hidden> wrote:
>> ---------- Forwarded message ----------
>> From: Tim Daly <address@hidden>
>> Date: Tue, 9 Jul 2019 22:56:24 -0400
>> Subject: Re: [EXTERNAL] Re: [Axiom-developer] Axiom's Sane redesign
>> musings
>> To: Martin Baker <address@hidden>
>>
>> Progress is being made. Axiom was written long before Common
>> Lisp existed. A lot of the code is due to translations from Maclisp
>> and LispVM.
>>
>> I'm moving the Axiom hierarchy to Common Lisp CLOS code.
>> This has several advantages.
>>
>> It eliminates the databases. They were created because there
>> was not enough memory (at 16 megabytes).
>>
>> It uses native code to do dispatch.
>>
>> CLOS defclass creates Common Lisp types so all of the code
>> is well-typed at the lisp level.
>>
>> CLOS is lisp so ordinary lisp code can use Axiom functions
>> directly. This makes Axiom into an "embeddable library".
>>
>> CLOS is the target language for the Axiom compiler. The
>> compiler is being re-architected to use nano passes [0] for
>> compiling. This will make it much easier to maintain in
>> the long term and much easier to extend.
>>
>> This technique allows building the compiler in stages from
>> running code to running code at every step.
>>
>> The new interpreter is much simpler as it just runs the CLOS
>> code directly.
>>
>> The choice of logic and specification languages are still unclear.
>> These will also be created first at the lisp level and then covered
>> by the compiler with additional nano-passes.
>>
>> Anyway, coding has begun.
>>
>> Tim
>>
>> [0]  Sarker, Dipanwita and Waddell, Oscar and Kybvig, R. Kent
>> "A Nanopass Framework for Compiler Education" (2004)
>>
>>
>> On 6/30/19, Tim Daly <address@hidden> wrote:
>>> There are thousands of hours of expertise and thousands of
>>> functions embedded in Spad code. An important design goal
>>> is to ensure that code continues to function. The Sane compiler
>>> will output code that runs in the interpreter. It is important that
>>> "nothing breaks".
>>>
>>> That said, the Sane compiler is "layered". The core of the design
>>> is that Axiom categories, domains, and packages are represnted
>>> as lisp classes and instances. This "core" is essentially what the
>>> compiler people call an Abstract Syntax Tree (AST). But in this
>>> case it is much more than syntax.
>>>
>>> Given this "core" there are several tasks.
>>>
>>> 1) compile spad code to the core. The "front end" should
>>> accept and understand current Spad code, unwinding it
>>> into the core class structure.
>>>
>>> 2) compile core classes to Axiom data structures. Thi
>>> "back end" generates current Axiom data structures from
>>> the core data structures.
>>>
>>> Now the compiler generates working code yet is in a state
>>> to accept enhancements, essentially by extending the core
>>> class objects.
>>>
>>> 3) In the interpreter, modify the getdatabase function to
>>> extract data from the core rather than the databases. So
>>> the databases go away but the interpreter continues to work.
>>>
>>> So now the interpreter has been "lifted" onto the core classes
>>> but continues to function.
>>>
>>> 4) enhance the core to support the axioms / specifications /
>>> proofs /etc. This involves adding fields to the lisp classes.
>>> This core work gives additional fields to hold information.
>>>
>>> 5) extend the Spad language (Spad 2.0?) to handle the
>>> additional axioms / specifications / proofs / etc. This
>>> involves adding syntax to the Spad language to support
>>> the new fields.
>>>
>>> 6) build back-end targets to proof systems, spec systems,
>>> etc. Compilers like GCC have multiple back ends. The Sane
>>> compiler targets the interpreter, a specification checker, a
>>> proof system, etc. as separate back ends, all from the same
>>> core structures.
>>>
>>> The Compiler Design
>>>
>>> A separate but parallel design goal is to build the compiler so
>>> it can be type-checked. Each function has typed input and
>>> typed output and is, for the most part, purely functional. So,
>>> for example, a "Filename" is an instance of a "File" object.
>>> A "Line" is an instance of "String". The "FileReader" is
>>>
>>> FileReader : Filename -> List Line
>>>
>>> Careful design of the language used to construct hte compiler
>>> (as opposed to the Spad language it accepts) makes it easier
>>> to type check the compiler itself.
>>>
>>> By REALLY careful design, the types are build on a layered
>>> subset of lisp, like Milawa
>>> https://urldefense.proofpoint.com/v2/url?u=https-3A__www.cl.cam.ac.uk_-7Emom22_soundness.pdf&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=vSWzY44D3q0ZbuiiWC71z-d0735kVc-z56JhhJvTxWk&s=hlB5Qn3wSwx2kqsIJIM6yL63N8pGP_FZJQWPvOz_Anw&e=
>>> which is sound all the way down to the metal.
>>>
>>> It all goes in stages. Build the new core class structure in a
>>> strongly typed fashion. Accept the Spad language. Generate
>>> Interpreter code. Enhance the core to support proofs / specs.
>>> Enhance the language to support proofs / specs. Accept the
>>> new language. Generate back ends to target the interpreter
>>> and a proof / spec system. Build it all on a sound base so
>>> the compiler can be checked.
>>>
>>> To the initial end user, the Sane version is the same as the
>>> current system. But in the long term all of the Axiom code
>>> could be called from any Lisp function. The Sane version
>>> can also be used as an "Oracle" for proof systems, since
>>> the code has been proven correct.
>>>
>>> This is a huge project but it can be done in small steps.
>>> In particular, the goal is to build a "thin thread" all the way
>>> through the system to handle only the GCD algorithms.
>>> Once that proof happens "the real work begins".
>>>
>>> Tim
>>>
>>>
>>>
>>>
>>> On 6/30/19, Martin Baker <address@hidden> wrote:
>>>> Tim,
>>>>
>>>> This all seems to be about the lisp layer, obviously thats what
>>>> interests you.
>>>>
>>>> It seems to me that if SPAD code is complicated and not aligned to type
>>>> theory then, when SPAD is complied to Lisp, the List code will be
>>>> complicated and hard to work with. Your previous remarks, about not
>>>> seeing the whole elephant, suggest to me that you are drowning in
>>>> complexity. Most languages, in their lifetime, acquire some messiness
>>>> that needs to be cleared out occasionally.
>>>>
>>>> Don't you think its time for SPAD 2.0 ?
>>>>
>>>> Martin
>>>>
>>>> On 30/06/2019 02:17, Tim Daly wrote:
>>>>> One major Sane design decision is the use of CLOS,
>>>>> the Common Lisp Object System.
>>>>>
>>>>> First, since each CLOS object is a type it is possible to
>>>>> create strong types everywhere. This helps with the ultimate
>>>>> need to typecheck the compiler and the generated code.
>>>>>
>>>>> Second, CLOS is an integral part of common lisp. One of
>>>>> the Sane design goals is to make it possible to use Axiom's
>>>>> domains in ordinary lisp programs. Since Axiom is nothing
>>>>> more than a domain specific language on common lisp it
>>>>> makes sense to construct it so users can freely intermix
>>>>> polynomials with non-algebraic code.
>>>>>
>>>>> Third, CLOS is designed for large program development,
>>>>> hiding most of the implementation details and exposing
>>>>> a well-defined API. This will make future maintenance and
>>>>> documentation of Axiom easier, contributing to its longer
>>>>> intended life.
>>>>>
>>>>> So for a traditional Axiom user nothing seems to have
>>>>> changed. But for future users it will be easy to compute
>>>>> an integral in the middle of regular programs.
>>>>>
>>>>> Tim
>>>>>
>>>>> On 6/27/19, Tim Daly <address@hidden> wrote:
>>>>>> Another thought....
>>>>>>
>>>>>> There has been a "step change" in computer science in the last few
>>>>>> years.
>>>>>>
>>>>>> Guy Steele did a survey of the use of logic notation in conference
>>>>>> papers.
>>>>>> More than 50% of the papers in some conferences use logic notation
>>>>>> (from one of the many logics).
>>>>>>
>>>>>> CMU teaches their CS courses all based on and requiring the use of
>>>>>> logic and the associated notation. My college mathematics covered
>>>>>> the use of truth tables. The graduate course covered the use of
>>>>>> Karnaugh maps.
>>>>>>
>>>>>> Reading current papers, I have found several papers with multiple
>>>>>> pages containing nothing but "judgements", pages of greek notation.
>>>>>> If you think Axiom's learning curve is steep, you should look at
>>>>>> Homotopy Type Theory (HoTT).
>>>>>>
>>>>>> I taught a compiler course at Vassar in the previous century but
>>>>>> the Dragon book didn't cover CIC in any detail and I would not
>>>>>> have understood it if it did.
>>>>>>
>>>>>> The original Axiom software predates most of the published logic
>>>>>> papers, at least as they applied to software. Haskell Curry wrote
>>>>>> from the logic side in 1934 and William Howard published in 1969
>>>>>> but I only heard of the Curry-Howard correspondence in 1998.
>>>>>>
>>>>>> Writing a compiler these days requires the use of this approach.
>>>>>> In all, that's a good thing as it makes it clear how to handle types
>>>>>> and how to construct software that is marginally more correct.
>>>>>>
>>>>>> The new Sane compiler is building on these logic foundations,
>>>>>> based on the Calculus of Inductive Construction and Dependent
>>>>>> Type theory. The compiler itself is strongly typed as is the
>>>>>> language it supports.
>>>>>>
>>>>>> Since dependent types are not decidable there will always be
>>>>>> heuristics at runtime to try to disambiguate types, only now we
>>>>>> will have to write the code in greek :-)
>>>>>>
>>>>>> Tim
>>>>
>>>
>>
>
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> https://urldefense.proofpoint.com/v2/url?u=https-3A__lists.nongnu.org_mailman_listinfo_axiom-2Ddeveloper&d=DwIGaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=vSWzY44D3q0ZbuiiWC71z-d0735kVc-z56JhhJvTxWk&s=VFM7ohCxqRASi69pd3rtVjCg7DpNpqSP3M74R5bOO20&e=