Axiom musings...

Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Axiom musings...

Tim Daly
Jason Gross and Adam Chlipala ("Parsing Parses") developed
a dependently typed general parser for context free grammar
in Coq.

They used the parser to prove its own completeness.

Unfortunately Spad is not a context-free grammar.
But it is an intersting thought exercise to consider
an "Axiom on Coq" implementation.

Tim

Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Tim Daly
The current design and code base (in bookvol15) supports
multiple back ends. One will clearly be a common lisp.

Another possible design choice is to target the GNU
GCC intermediate representation, making Axiom "just
another front-end language" supported by GCC.

The current intermediate representation does not (yet)
make any decision about the runtime implementation.

Tim


On 11/26/19, Tim Daly <[hidden email]> wrote:

> Jason Gross and Adam Chlipala ("Parsing Parses") developed
> a dependently typed general parser for context free grammar
> in Coq.
>
> They used the parser to prove its own completeness.
>
> Unfortunately Spad is not a context-free grammar.
> But it is an intersting thought exercise to consider
> an "Axiom on Coq" implementation.
>
> Tim
>

Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Tim Daly
The new Sane compiler is also being tested with the Fricas
algebra code. The compiler knows about the language but
does not depend on the algebra library (so far). It should be
possible, by design, to load different algebra towers.

In particular, one idea is to support the "tiny theories"
algebra from Carette and Farmer. This would allow much
finer grain separation of algebra and axioms.

This "flexible algebra" design would allow things like the
Lean theorem prover effort in a more natural style.

Tim


On 11/26/19, Tim Daly <[hidden email]> wrote:

> The current design and code base (in bookvol15) supports
> multiple back ends. One will clearly be a common lisp.
>
> Another possible design choice is to target the GNU
> GCC intermediate representation, making Axiom "just
> another front-end language" supported by GCC.
>
> The current intermediate representation does not (yet)
> make any decision about the runtime implementation.
>
> Tim
>
>
> On 11/26/19, Tim Daly <[hidden email]> wrote:
>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>> a dependently typed general parser for context free grammar
>> in Coq.
>>
>> They used the parser to prove its own completeness.
>>
>> Unfortunately Spad is not a context-free grammar.
>> But it is an intersting thought exercise to consider
>> an "Axiom on Coq" implementation.
>>
>> Tim
>>
>

Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Tim Daly
I'm still undecided about accepting unicode on input as opposed
to latex-style input (e.g. \pi vs the unicode pi character).

The logic syntax would really benefit from using things like
\forall as a unicode character on input.

It makes the math I/O much prettier but it makes parsing
much harder. What does one do with a function
  (code-char 958)(x:INT) ==

aka (greek small letter xi)....

Some experiments are "in the thought pipeline"....

Tim


On 11/27/19, Tim Daly <[hidden email]> wrote:

> The new Sane compiler is also being tested with the Fricas
> algebra code. The compiler knows about the language but
> does not depend on the algebra library (so far). It should be
> possible, by design, to load different algebra towers.
>
> In particular, one idea is to support the "tiny theories"
> algebra from Carette and Farmer. This would allow much
> finer grain separation of algebra and axioms.
>
> This "flexible algebra" design would allow things like the
> Lean theorem prover effort in a more natural style.
>
> Tim
>
>
> On 11/26/19, Tim Daly <[hidden email]> wrote:
>> The current design and code base (in bookvol15) supports
>> multiple back ends. One will clearly be a common lisp.
>>
>> Another possible design choice is to target the GNU
>> GCC intermediate representation, making Axiom "just
>> another front-end language" supported by GCC.
>>
>> The current intermediate representation does not (yet)
>> make any decision about the runtime implementation.
>>
>> Tim
>>
>>
>> On 11/26/19, Tim Daly <[hidden email]> wrote:
>>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>>> a dependently typed general parser for context free grammar
>>> in Coq.
>>>
>>> They used the parser to prove its own completeness.
>>>
>>> Unfortunately Spad is not a context-free grammar.
>>> But it is an intersting thought exercise to consider
>>> an "Axiom on Coq" implementation.
>>>
>>> Tim
>>>
>>
>

Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Jacques Carette
In reply to this post by Tim Daly
The underlying technology to use for building such an algebra library is
documented in the paper " Building on the Diamonds between Theories:
Theory Presentation Combinators"
http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which will
also be on the arxiv by Monday, and has been submitted to a journal].

There is a rather full-fledged prototype, very well documented at
https://alhassy.github.io/next-700-module-systems/prototype/package-former.html 
(source at https://github.com/alhassy/next-700-module-systems). It is
literate source.

The old prototype was hard to find - it is now at
https://github.com/JacquesCarette/MathScheme.

There is also a third prototype in the MMT system, but it does not quite
function properly today, it is under repair.

The paper "A Language Feature to Unbundle Data at Will"
(https://alhassy.github.io/next-700-module-systems/papers/gpce19_a_language_feature_to_unbundle_data_at_will.pdf)
is also relevant, as it solves a problem with parametrized theories
(parametrized Categories in Axiom terminology) that all current systems
suffer from.

Jacques

On 2019-11-27 11:47 p.m., Tim Daly wrote:

> The new Sane compiler is also being tested with the Fricas
> algebra code. The compiler knows about the language but
> does not depend on the algebra library (so far). It should be
> possible, by design, to load different algebra towers.
>
> In particular, one idea is to support the "tiny theories"
> algebra from Carette and Farmer. This would allow much
> finer grain separation of algebra and axioms.
>
> This "flexible algebra" design would allow things like the
> Lean theorem prover effort in a more natural style.
>
> Tim
>
>
> On 11/26/19, Tim Daly <[hidden email]> wrote:
>> The current design and code base (in bookvol15) supports
>> multiple back ends. One will clearly be a common lisp.
>>
>> Another possible design choice is to target the GNU
>> GCC intermediate representation, making Axiom "just
>> another front-end language" supported by GCC.
>>
>> The current intermediate representation does not (yet)
>> make any decision about the runtime implementation.
>>
>> Tim
>>
>>
>> On 11/26/19, Tim Daly <[hidden email]> wrote:
>>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>>> a dependently typed general parser for context free grammar
>>> in Coq.
>>>
>>> They used the parser to prove its own completeness.
>>>
>>> Unfortunately Spad is not a context-free grammar.
>>> But it is an intersting thought exercise to consider
>>> an "Axiom on Coq" implementation.
>>>
>>> Tim
>>>

Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Tim Daly
The Axiom Sane compiler is being "shaped by the hammer
blows of reality", to coin a phrase.

There are many goals. One of the primary goals is creating a
compiler that can be understood, maintained, and modified.

So the latest changes involved adding multiple index files.
These are documentation (links to where terms are mentioned
in the text), code (links to the implementation of things),
error (links to where errors are defined), signatures (links to
the signatures of lisp functions), figures (links to figures),
and separate category, domain, and package indexes.

The tikz package is now used to create "railroad diagrams"
of syntax (ala, the PASCAL report). The implementation of
those diagrams follows immediately. Collectively these will
eventually define at least the syntax of the language. In the
ideal, changing the diagram would change the code but I'm
not that clever.

Reality shows up with the curent constraint that the
compiler should accept the current Spad language as
closely as possible. Of course, plans are to include new
constructs (e.g. hypothesis, axiom, specification, etc)
but these are being postponed until "syntax complete".

All parse information is stored in a parse object, which
is a CLOS object (and therefore a Common Lisp type)
Fields within the parse object, e.g. variables are also
CLOS objects (and therefore a Common Lisp type).
It's types all the way down.

These types are being used as 'signatures' for the
lisp functions. The goal is to be able to type-check the
compiler implementation as well as the Sane language.

The parser is designed to "wrap around" so that the
user-level output of a parse should be the user-level
input (albeit in a 'canonical" form). This "mirror effect"
should make it easy to see that the parser properly
parsed the user input.

The parser is "first class" so it will be available at
runtime as a domain allowing Spad code to construct
Spad code.

One plan, not near implementation, is to "unify" some
CLOS types with the Axiom types (e.g. String). How
this will happen is still in the land of design. This would
"ground" Spad in lisp, making them co-equal.

Making lisp "co-equal" is a feature, especially as Spad is
really just a domain-specific language in lisp. Lisp
functions (with CLOS types as signatures) would be
avaiable for implementing Spad functions. This not
only improves the efficiency, it would make the
BLAS/LAPACK (see volume 10.5) code "native" to Axiom.
.
On the theory front I plan to attend the Formal Methods
in Mathematics / Lean Together conference, mostly to
know how little I know, especially that I need to know.
http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/

Tim



On 11/28/19, Jacques Carette <[hidden email]> wrote:

> The underlying technology to use for building such an algebra library is
> documented in the paper " Building on the Diamonds between Theories:
> Theory Presentation Combinators"
> http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which will
> also be on the arxiv by Monday, and has been submitted to a journal].
>
> There is a rather full-fledged prototype, very well documented at
> https://alhassy.github.io/next-700-module-systems/prototype/package-former.html
>
> (source at https://github.com/alhassy/next-700-module-systems). It is
> literate source.
>
> The old prototype was hard to find - it is now at
> https://github.com/JacquesCarette/MathScheme.
>
> There is also a third prototype in the MMT system, but it does not quite
> function properly today, it is under repair.
>
> The paper "A Language Feature to Unbundle Data at Will"
> (https://alhassy.github.io/next-700-module-systems/papers/gpce19_a_language_feature_to_unbundle_data_at_will.pdf)
>
> is also relevant, as it solves a problem with parametrized theories
> (parametrized Categories in Axiom terminology) that all current systems
> suffer from.
>
> Jacques
>
> On 2019-11-27 11:47 p.m., Tim Daly wrote:
>> The new Sane compiler is also being tested with the Fricas
>> algebra code. The compiler knows about the language but
>> does not depend on the algebra library (so far). It should be
>> possible, by design, to load different algebra towers.
>>
>> In particular, one idea is to support the "tiny theories"
>> algebra from Carette and Farmer. This would allow much
>> finer grain separation of algebra and axioms.
>>
>> This "flexible algebra" design would allow things like the
>> Lean theorem prover effort in a more natural style.
>>
>> Tim
>>
>>
>> On 11/26/19, Tim Daly <[hidden email]> wrote:
>>> The current design and code base (in bookvol15) supports
>>> multiple back ends. One will clearly be a common lisp.
>>>
>>> Another possible design choice is to target the GNU
>>> GCC intermediate representation, making Axiom "just
>>> another front-end language" supported by GCC.
>>>
>>> The current intermediate representation does not (yet)
>>> make any decision about the runtime implementation.
>>>
>>> Tim
>>>
>>>
>>> On 11/26/19, Tim Daly <[hidden email]> wrote:
>>>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>>>> a dependently typed general parser for context free grammar
>>>> in Coq.
>>>>
>>>> They used the parser to prove its own completeness.
>>>>
>>>> Unfortunately Spad is not a context-free grammar.
>>>> But it is an intersting thought exercise to consider
>>>> an "Axiom on Coq" implementation.
>>>>
>>>> Tim
>>>>
>

Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Tim Daly
I've been reading Stephen Kell's (Univ of Kent
https://www.cs.kent.ac.uk/people/staff/srk21/) on
Seven deadly sins of talking about “types”
https://www.cs.kent.ac.uk/people/staff/srk21//blog/2014/10/07/

He raised an interesting idea toward the end of the essay
that type-checking could be done outside the compiler.

I can see a way to do this in Axiom's Sane compiler.
It would be possible to run a program over the source code
to collect the information and write a stand-alone type
checker. This "unbundles" type checking and compiling.

Taken further I can think of several other kinds of checkers
(aka 'linters') that could be unbundled.

It is certainly something to explore.

Tim


On 12/8/19, Tim Daly <[hidden email]> wrote:

> The Axiom Sane compiler is being "shaped by the hammer
> blows of reality", to coin a phrase.
>
> There are many goals. One of the primary goals is creating a
> compiler that can be understood, maintained, and modified.
>
> So the latest changes involved adding multiple index files.
> These are documentation (links to where terms are mentioned
> in the text), code (links to the implementation of things),
> error (links to where errors are defined), signatures (links to
> the signatures of lisp functions), figures (links to figures),
> and separate category, domain, and package indexes.
>
> The tikz package is now used to create "railroad diagrams"
> of syntax (ala, the PASCAL report). The implementation of
> those diagrams follows immediately. Collectively these will
> eventually define at least the syntax of the language. In the
> ideal, changing the diagram would change the code but I'm
> not that clever.
>
> Reality shows up with the curent constraint that the
> compiler should accept the current Spad language as
> closely as possible. Of course, plans are to include new
> constructs (e.g. hypothesis, axiom, specification, etc)
> but these are being postponed until "syntax complete".
>
> All parse information is stored in a parse object, which
> is a CLOS object (and therefore a Common Lisp type)
> Fields within the parse object, e.g. variables are also
> CLOS objects (and therefore a Common Lisp type).
> It's types all the way down.
>
> These types are being used as 'signatures' for the
> lisp functions. The goal is to be able to type-check the
> compiler implementation as well as the Sane language.
>
> The parser is designed to "wrap around" so that the
> user-level output of a parse should be the user-level
> input (albeit in a 'canonical" form). This "mirror effect"
> should make it easy to see that the parser properly
> parsed the user input.
>
> The parser is "first class" so it will be available at
> runtime as a domain allowing Spad code to construct
> Spad code.
>
> One plan, not near implementation, is to "unify" some
> CLOS types with the Axiom types (e.g. String). How
> this will happen is still in the land of design. This would
> "ground" Spad in lisp, making them co-equal.
>
> Making lisp "co-equal" is a feature, especially as Spad is
> really just a domain-specific language in lisp. Lisp
> functions (with CLOS types as signatures) would be
> avaiable for implementing Spad functions. This not
> only improves the efficiency, it would make the
> BLAS/LAPACK (see volume 10.5) code "native" to Axiom.
> .
> On the theory front I plan to attend the Formal Methods
> in Mathematics / Lean Together conference, mostly to
> know how little I know, especially that I need to know.
> http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/
>
> Tim
>
>
>
> On 11/28/19, Jacques Carette <[hidden email]> wrote:
>> The underlying technology to use for building such an algebra library is
>> documented in the paper " Building on the Diamonds between Theories:
>> Theory Presentation Combinators"
>> http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which will
>> also be on the arxiv by Monday, and has been submitted to a journal].
>>
>> There is a rather full-fledged prototype, very well documented at
>> https://alhassy.github.io/next-700-module-systems/prototype/package-former.html
>>
>> (source at https://github.com/alhassy/next-700-module-systems). It is
>> literate source.
>>
>> The old prototype was hard to find - it is now at
>> https://github.com/JacquesCarette/MathScheme.
>>
>> There is also a third prototype in the MMT system, but it does not quite
>> function properly today, it is under repair.
>>
>> The paper "A Language Feature to Unbundle Data at Will"
>> (https://alhassy.github.io/next-700-module-systems/papers/gpce19_a_language_feature_to_unbundle_data_at_will.pdf)
>>
>> is also relevant, as it solves a problem with parametrized theories
>> (parametrized Categories in Axiom terminology) that all current systems
>> suffer from.
>>
>> Jacques
>>
>> On 2019-11-27 11:47 p.m., Tim Daly wrote:
>>> The new Sane compiler is also being tested with the Fricas
>>> algebra code. The compiler knows about the language but
>>> does not depend on the algebra library (so far). It should be
>>> possible, by design, to load different algebra towers.
>>>
>>> In particular, one idea is to support the "tiny theories"
>>> algebra from Carette and Farmer. This would allow much
>>> finer grain separation of algebra and axioms.
>>>
>>> This "flexible algebra" design would allow things like the
>>> Lean theorem prover effort in a more natural style.
>>>
>>> Tim
>>>
>>>
>>> On 11/26/19, Tim Daly <[hidden email]> wrote:
>>>> The current design and code base (in bookvol15) supports
>>>> multiple back ends. One will clearly be a common lisp.
>>>>
>>>> Another possible design choice is to target the GNU
>>>> GCC intermediate representation, making Axiom "just
>>>> another front-end language" supported by GCC.
>>>>
>>>> The current intermediate representation does not (yet)
>>>> make any decision about the runtime implementation.
>>>>
>>>> Tim
>>>>
>>>>
>>>> On 11/26/19, Tim Daly <[hidden email]> wrote:
>>>>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>>>>> a dependently typed general parser for context free grammar
>>>>> in Coq.
>>>>>
>>>>> They used the parser to prove its own completeness.
>>>>>
>>>>> Unfortunately Spad is not a context-free grammar.
>>>>> But it is an intersting thought exercise to consider
>>>>> an "Axiom on Coq" implementation.
>>>>>
>>>>> Tim
>>>>>
>>
>