[Top][All Lists]

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

Re: Axiom musings...

From: Tim Daly
Subject: Re: Axiom musings...
Date: Thu, 28 Nov 2019 00:28:45 -0500

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


On 11/27/19, Tim Daly <address@hidden> 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 <address@hidden> 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 <address@hidden> 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 via email to

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