[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Call for help
From: |
daly |
Subject: |
Re: [Axiom-developer] Call for help |
Date: |
Mon, 27 Jul 2015 08:30:54 -0500 |
>This goes back to pop! ; it would seem that push/pop is an abstract
>logical idea and shouldn't be specialized with different versions for
>each domain/catagory. I might like to temporarily push/pop one of the
>elements of the above, infinite, Euclidean domains during calculations
>for GCD and not have to rewrite push/pop with all the hazards that
>carries. In addition I would have to rely on some abstract
>delineation to prove that my new code was "correct". So the abstract
>idea and proof has to be abstract and domain free to be coherent.
You're correct that a full proof should be abstract and domain free. But
while proving the general case might be possible, a proof might only be
available for a specific function in a specific domain.
The generalization suggested last time was to add an "assuming"
clause, of the form,
)abbrev category FOO Foo
Foo: Category == Bar with
sig1
sig2
== add
sig1 == ...
assuming
AssociativeAxiom:
CommuativeAxiom:
Proviso1:
Definition1:
However, within a domain a single function might be easily proven.
It might make sense to extend the syntax of == definitions to admit
a proof clause, e.g.
fn(a:Integer,b:Integer) ==
someop(a,b)
proof:
...
Tim
- Re: [Axiom-developer] Call for help, (continued)
- Re: [Axiom-developer] Call for help, Kurt Pagani, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/25
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/26
- Re: [Axiom-developer] Call for help, daly, 2015/07/27
- Re: [Axiom-developer] Call for help,
daly <=
- Re: [Axiom-developer] Call for help, daly, 2015/07/27