gt;>>>> philosophy,
>>>>> [1]
>>>>> <https://en.wikipedia.org/wiki/Principia_Mathematica#cite_note-SEP-1>
>>>>> being
>>>>> one of the foremost products of the belief that such an undertaking may be
>>>>> achievable. However, in 1931, Gödel'
run.com
>>>>> /products/provenvisor/nxp/
>>>>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www.provenrun.com_products_provenvisor_nxp_&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=KxTLI8x_XL
lt;https://en.wikipedia.org/wiki/Real_numbers>. Deeper theorems from real
>>> analysis <https://en.wikipedia.org/wiki/Real_analysis> were not
>>> included, but by the end of the third volume it was clear to experts that a
>>> large amount of known mathematics cou
me on the foundations of geometry
>> <https://en.wikipedia.org/wiki/Geometry> had been planned, but the
>> authors admitted to intellectual exhaustion upon completion of the third."
>>
>>
>> Perhaps someday, a more powerful computer system than Coq can rep
It is also why I
> admire your tenacity to follow your goal. Despite Gödel
> <https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorem>'s
> incompleteness theorem, we need to prove correctness (of Axiom) as deep and
> wide as we can, and there are many ways to do
nor is there sufficient interest in the
> hardware industry to provide that level of research). Note that the
> industry is still satisfied with "ad-hoc solutions" (and that might mean
> patches, and we all know how error-prone those are---so much so that people
> learn and r
William,
I understand the issue of proving "down to the metal".
Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.
http://axiom-developer.org/axiom-website/bookvol1
William,
That's an interesting reply. In general, I agree with the points you make.
Some overall comments are in order. For the last 18 months I've been working
with people at Carnegie Mellon in Computer Science. One thing that really
stands out is that virtually all the courses have a strong emp
Tim,
I've been experimenting with a language called 'Idris'. I've been
playing around with writing some of the Axiom SPAD library code in
Idris. My code so far is here:
https://github.com/martinbaker/Idris-dev/tree/algebra/libs/algebra
Nothing usable yet, I'm just experimenting with whats invo
Yes, I'd like to have a solid "floor" to the proofs and the fewer layers,
the better.
An issue arises when looking to prove the propositions for the Domain
NonNegativeInteger (NNI). This is closely related to the 'nat' domain in
proof
systems. However, NNI relies on calls to Lisp for things like d
I previously mentioned the "proof tower" approach to the question
of proving code at many different layers. Spad code proven in COQ,
Lisp code in ACL2, and Intel code in CCAs. The missing step in the
tower was C.
Apparently there is work in COQ (http://robbertkrebbers.nl/research/ch2o/)
on the CH2
>Perhaps there are issues around this that will matter? Given that there
>are two formulations of each algebra, one like this:
>zero: () -> $
>succ: ($) -> $
>and one like this:
>+ ($,$) -> $
>If one form is needed for inductive proofs and the other form for
>applied mathematics. Could Axiom ho
On 31/03/17 05:34, Tim Daly wrote:
Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does n
Renaud,
I've been looking at FoCal and, in particular, the Zenon program
http://zenon.inria.fr/zenlpar07.pdf
Zenon appears to be able to output OCAML code from proofs.
In your opinion is it reasonable to consider modifying the back end
to output Spad code?
Tim
On Fri, Feb 10, 2017 at 8:39 AM,
Renaud,
I'm just getting around to the FoCal information. Obviously you've done a
lot of
work on this subject already. I have the papers and the reference manual
near
the top of the reading stack. I'm certain to have questions.
Yes, BasicType requires properties for = such as symmetry which would
Dear Axiom gurus,
Axiom's NNI inherits from a dozen Category objects, one of which
is BasicType which contains two signatures:
?=?: (%,%) -> Boolean ?~=?: (%,%) -> Boolean
In the ideal case we would decorate BasicType with the existing
definitions of = and ~= so we could create a new li
Termination is clearly an issue for provers like Coq. There are
solutions to define function partially but they have some cost in term
of proof effo. Maybe we could benefit how the people of Focal deals
with loops.
--
Laurent
On 02/09/2017 04:54 AM, Tim Daly wrote:
> Coq provides gc
>
> > Coq provides gcd as
> >
> > Fixpoint gcd a b :=
> >match a with
> > | 0 => b
> > | S a' => gcd (b mod (S a')) (S a')
> >end.
>
> > and Axiom's definition is
>
> > gcd(x:NNI,y:NNI):NNI ==
> >zero? x => y
> >gcd(y rem x, x)
>
> > Everything in Spad is strongly typed
>Is there anything that requires that the operation you implement is
>reflexive, symmetric, and transitive? Putting axioms on the structure
>specifies that that has to be the case. Without such axioms, you
>cannot prove anything about implementations in general. You can
>only prove things about in
On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly wrote:
> Part of your struggle of understanding what I wrote is that I'm not yet
> fluent in the
> logic language and syntax. I'm learning as fast as I can so please be
> patient.
>
> ==
> CATEGORY SIGNAT
Am 08.02.2017 um 15:29 schrieb Tim Daly:
> The game is to prove GCD in NonNegativeInteger (NNI).
We encounter numerous problems when trying to prove gcd from EuclideanDomain:
---
gcd(x, y) == --Euclidean Algorithm
x := unitCanonical x
y := unitCanonical y
while not zero? y repeat
(x,
Part of your struggle of understanding what I wrote is that I'm not yet
fluent in the
logic language and syntax. I'm learning as fast as I can so please be
patient.
==
CATEGORY SIGNATURE vs DOMAIN SEMANTICS
> Presumably you will eventually want
Dear Tim,
I don't understand what you mean. For one thing, theorems in both Lean and
Coq are marked as opaque, since you generally don't care about the
contents. But even if we replace "theorem" by "definition," I don't know
what you imagine going into the "...".
I think what you want to do is re
I got the tongue-in-cheek aspect but Axiom's formal logic basis is
important.
In the 1980s Expert Systems were going to take over the world. We tried to
prove our version
correct using the Boyer-Moore theorem proving technology. We failed
miserably, partly
because the technology was not up to the
I was largely poking, tongue in cheek, at the earlier syllogism:
>> The point is that Lisp has a formal logic basis and, as Spad is really
>> just a domain specific language implemented in Lisp then Spad shares
>> the formal logic basis.
-- Gaby
On Thu, Jan 12, 2017 at 10:35 PM, Tim Daly wrote:
>From: Kurt Pagani
>
>>
>> Axiom is using Coq for its proof platform because Axiom needs
>> dependent types (e.g. specifying matrix sizes by parameters).
>>
>> In addition, Coq is capable of generating a program from a
>> proof and the plan is to reshape the Spad solution to more
>> closely mirror
Am 13.01.2017 um 07:35 schrieb Tim Daly:
...
>
> Axiom is using Coq for its proof platform because Axiom needs
> dependent types (e.g. specifying matrix sizes by parameters).
>
> In addition, Coq is capable of generating a program from a
> proof and the plan is to reshape the Spad solution to m
> There were implementations of C in Lisp. So C shares that formal logic
basis, or that it was discovered?
According to Wadler, C is an "invented" language, not a "discovered"
language.
Wadler (https://www.youtube.com/watch?v=aeRVdYN6fE8) at around 40 minutes
shows the logician's view versus the
There were implementations of C in Lisp. So C shares that formal logic
basis, or that it was discovered?
On Wed, Jan 11, 2017 at 8:17 PM, Tim Daly wrote:
> I'm making progress on proving Axiom correct both at the Spad level and
> the Lisp level. One interesting talk by Phillip Wadler on "Proposi
Greetings! I am considering pushing some pathname ansi fixes from
master into the upcoming gcl release. This has exposed an axiom issue.
#'pathname cannot take a symbol argument.
Here is a patch, which I think is backward compatible (testing):
--- axiom-20140801.orig/books/bookvol5.pamphlet
+
Great! Actually this list makes a great dictionary for me :)
Might I suggest opening an axiom-developer forum where discussions about
different categories, proofs, and typos can be addressed
individually? And perhaps a prefered format for the signatures along
the ideas of input-process-out
Hi Tim
that's great, indeed. Coq also seems to me best suited for this
challenging task, however, I would suggest to use "the mathematical
proof language (MPL)" as described in chapeter 11 of the reference
manual. It's a matter of taste, of courese, but imho MPL is much more
readable (at least to
32 matches
Mail list logo
