erhaps 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
meritus
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
on behalf of Tim
Daly
Sent: Friday, July 12, 2019 5:11 AM
To: axiom-dev
Subject: Re: [Axiom-devel
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
On Sun, Jun 30, 2019 at 11:40 AM Tim Daly wrote:
>
> By REALLY careful design, the types are build on a layered
> subset of lisp, like Milawa
> https://www.cl.cam.ac.uk/~mom22/soundness.pdf
> which is sound all the way down to the metal.
>
Milawa and Jitawa... Wow. That is a really interesting
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
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
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
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
Yes, but even more than that.
The goal is to make Axiom a "trusted system" for the whole of
computational mathematics.
To do this, consider this (not entirely random) collection of systems
and facts:
1) Trusted systems are built using the de Bruijn principle. See, for example,
Tim,
When I read this I am picking up a slightly different flavor than what I
got from your first message in the thread.
You first message seemed to me to be about "merging computer algebra and
proof technology" but this message seems to be about running the two in
parallel.
I really like
Martin,
My current "line of attack" on this research is to try to prove the
GCD algorithm in NonNegativeInteger.
While this seems trivial in proof systems it is expensive to
compute from the inductive definition. While this seems
trivial in computer algebra, the implementation code lacks
proof.
On 6/25/19, William Sit wrote:
> The expression x = x + 0, whether treated as a type or an equation,
> can only make sense when x, =, + and 0 are clearly typed and defined.
> It makes little sense to me that this, as an equation, can be "proved"
> to be valid universally (that is, without the
It is all rather confusing. There are well over 100 "logics".
Equational logic, or equational reasoning, is a very restricted
logic having only equality as an operation.
An alternative interpretation would be a substitution-style
logic where equals can be substituted for equals as one of
the
Dear Martin and Tim:
The expression x = x + 0, whether treated as a type or an equation, can only
make sense when x, =, + and 0 are clearly typed and defined. It makes little
sense to me that this, as an equation, can be "proved" to be valid universally
(that is, without the definition of,
14 matches
Mail list logo
