Hmm. The problem to be solved involves several parts.
Idris is of interest in PART 6, 7, and 8 below.
PART 1: We have the domain
We have GCD in NAT (axiom: NonNegativeInteger or NNI)
NonNegativeInteger is what Axiom calls a "Domain", which means
that it contains signatures, such as
quo : (%,%) -> %
rem : (%,%) -> %
gcd : (%,%) -> %
which says that gcd takes 2 NonNegativeIntegers (NATs) and
returns a NonNegativeInteger (NAT).
The NonNegativeInteger domain also includes information about
how its elements are represented.
PART 2: We have an implementation of gcd in the domain
The NNI domain contains an implementation of gcd:
gcd(x,y) ==
zero? x => y
gcd(y rem x,x)
PART 3: We have a way to inherit things for the domain
The NNI domain inherits properties from what Axiom
(unfortunately) calls Categories. Categories provide
additional signatures and default implementations.
PART 4: We have the FUNDAMENTAL PROBLEM
The PROBLEM to be solved is that we want to prove
that the above code for gcd is correct.
Of course, the first question is "correct with respect to..."
PART 5: We need a specification language
There needs to be a specification of the gcd function.
What are the properties it should fulfill?
What are the invariants?
What are the preconditions?
What are the postconditions?
Some parts of the specification will be inherited.
Which means we need a language for specification.
PART 6: We need a theorem language
Given a specification, what theorems are available?
Some theorems are inherited from the categories,
usually as axioms.
Some theorems and axioms are directly stated in
the NNI domain.
Some lemmas need to be added to the domain to help
the proof process.
Which means we need a language for theorems.
PART 7: We need a proof engine
Now that we have an implementation, a specification,
a collection of theorems and pre- and post-conditions,
lemmas, and invariants we need a proof.
Which engine will we use for the proof?
What syntax does it require?
Does it provide a verifier to re-check proofs?
PART 8: We need to prove many GCD algorithms
Axiom contains 22 signatures for gcd. For example,
it contains a gcd for polynomials. The above machinery
needs to support proofs in those domains also.
PART 9: LOOP
GOTO part 4 above, pick a new function, and repeat.
PART 10: ISSUES
PART 10a: "Down to the metal"
THere are a pile of "side issues". I'm re-implementing Axiom
using Common Lisp CLOS. THe defclass macro in CLOS
creates new Common Lisp types. This allows using the types
for type-checking (currently looking at bi-directional checking
algorithms)
Axiom sits on Common Lisp. There is a question of using a
"trusted core". I'm looking into Milawa
https://www.cl.cam.ac.uk/~mom22/soundness.pdf
with a deeply layered design.
I'm also looking at SEL4 on ARM
https://ts.data61.csiro.au/publications/nicta_full_text/3783.pdf
which is a trustworthy operating system.
I wrote a paper on the semantics of the Intel instruction set:
Daly, Timothy Intel Instruction Semantics Generator SEI/CERT Research
Report, March 2012
http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/intel/intel.pdf
so SEL4 on Intel is interesting.
PART 10b: Dependent type theory
Dependent types are undecidable. Axiom contains several
heuristics to resolve types at runtime. The heuristic type
algorithm needs to be explicit and declarative.
PART 10c: Size
Axiom contains about 10,000 algorithms in 1100 categories,
domains, and packages. This is going to take a while.
PART 10d: Mathematics
Many of the algorithms are partial. Many are PhD thesis
work (and hard to understand). Many are ad hoc and have
no mathematical specification.
PART 10e: Time
The target delivery date is April, 2023.
There is much to do.
Tim
On 9/21/19, Henri Tuhola <address@hidden> wrote:
Idris has a way to present equalities like this:
addition_unit : (a:Nat) -> (a + 0) = a
addition_s : (a,b:Nat) -> (a + S b) = S (a + b)
add_commutative : (a,b:Nat) -> (a + b = b + a)
They can be used to prove more things:
try_out : (x,y:Nat) -> ((x + 0) + y) = y + x
try_out x y = rewrite addition_unit x in add_commutative x y
It's rewriting the left expression to right expression, though you can
easily flip the direction. For clarity I show these few dissections:
try_out x y = ?a1
a1 : plus (plus x 0) y = plus y x
try_out x y = rewrite addition_unit x in ?a2
a2 : plus x y = plus y x
Idris has this feature called "Elaborator reflection". It allows you
to describe automated tactics for writing proofs/programs.
The "getGoal" and "getEnv" allow you to examine types in the context:
getGoal : Elab (TTName, TT)
getEnv : Elab (List (TTName, Binder TT))
The elaborator reflection also allows accessing the term rewriting. I
suppose that's all you need in order to write a program that
simplifies equations inside the type context?
-- Henri Tuhola
On Sat, 21 Sep 2019 at 11:50, Martin Baker <address@hidden> wrote:
I'm a fan of both Axiom and Idris. I think my ideal would be Axiom
mathematics build on top of the Idris type system.
The Axiom type system was incredibly advanced for its time but I suspect
the Idris type system has finally caught up and overtaken it? Correct me
if I'm wrong but I think the Axiom type system does not have the
following capabilities that Idris does:
* Enforcement of pure functions.
* Ability to flag a function as total as opposed to partial (automatic
in some cases).
* Universes (types of types hierarchy).
I'm no expert but I would have guessed these things would be almost
indispensable for proving Axiom correct?
Also Idris makes it far more practical to use these things, I don't
think Axiom can implement category theory constructs like monads. Also,
although both have dependent types, Axiom does not use them for say,
preventing the addition of a 2D vector to a 3D vector. In Idris this is
more likely to be compile time error than a runtime error, I know there
are theoretical limits to this but I think Idris has capabilities to
make this practical in more cases.
I don't pretend I know how an Idris type system could be used with Axiom
in practice. For instance I think the proofs Henri is talking about are
equalities in the type system (propositions as types). So how would
these equations relate to equations acted on by equation solvers (which
might be an element of some equation type). Could there be some way to
lift equations into the type system and back?
Sorry if I'm confusing things here but I just have an intuition that
there is something even more powerful here if all this could be put
together.
Martin
On 21/09/2019 04:28, Tim Daly wrote:
Axiom has type information everywhere. It is strongly
dependently typed. So give a Polynomial type, which
Axiom has, over a Ring or Field, such as
Polynomial(Integer) or Polynomial(Fraction(Integer))
we can use theorems from the Ring while proving
properties of Polynomials.
_______________________________________________
Axiom-developer mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/axiom-developer