For the last year =
the Axiom effort has focused on proving Axiom

correct. There has b=
een much progress on that front. Soon therehttps://www.youtube.com/watch?= v=3DIPNdsnRWBkk

Summer 2017.

Tim

--001a113e71fe4b58910561db29d2--
From MAILER-DAEMON Thu Jan 18 03:57:11 2018
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ec60V-0003YW-3S
for mharc-axiom-developer@gnu.org; Thu, 18 Jan 2018 03:57:11 -0500
Received: from eggs.gnu.org ([2001:4830:134:3::10]:35562)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from I'm a computational mathematician (CM) =
so I'm coming to the logic

area from left field (deep left, ou=
t by the fence). Thus my questionYou made the passing comment that proofs are mathematical

For instance, in= Axiom, Integers are:

(1) -> )show Integer

Integer is a domain constructor

Abbreviation for Integer is INT=20

This constructor is exposed in this frame.

Issue )edit bookvol10.3.pamphlet to see algebra source code for INT=20 ------------------------------- Operations --------------------------------

?*? : (%,%) -> %

?*? : (Integer,%) -> %

?*? : (PositiveInteger,%) -> %

?**? : (%,PositiveInteger= ) -> %

?+? : (%,%) -> %

?-? : (%,%) -> %

-? : % -> %

?<? : (%,%) -> Bool= ean

?<=3D? : (%,%) -> Boolean

?=3D? : (%,%) -> = Boolean

?>? : (%,%) -> Boolean

?>=3D? : (%,%) ->= ; Boolean

D : % -> %

D : (%,NonNegativeInteger= ) -> %

OMwrite : (%,Boolean) -> String

OMwrite : % -> String

1 : () -> %

0 : () -> %

?^? : (%,PositiveInteger) -> %

abs : % -> %

addmod : (%,%,%) -> %

associates? : (%,%) ->= Boolean

base : () -> %

binomial : (%,%) -> %

bit? : (%,%) -> Boolean

coerce : Integer -> %

coerce : % -> %

coerce : Integer -> %

coerce : % -> OutputForm

convert : % -> String

convert : % -> DoubleFloat

convert : % -> Float

convert : % -> Pattern(Integer)

convert : % -> InputFo= rm

convert : % -> Integer

copy : % -> %

dec : % -> %

differentiate : % -> %

even? : % -> Boolean

factor : % -> Factored= (%)

factorial : % -> %

gcd : List(%) -> %

gcd : (%,%) -> %

hash : % -> %

hash : % -> SingleInteger

inc : % -> %

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 ..... etc.

But that seems odd to me, in two ways. First, Proofs seem more like

Polynomials. Polynomials don't have any meaning until you specify th= e

Once you give me the base ring I know what operations I=
can perform.

Proofs seem to need the set of sequents and=
the set of hypotheses in

order to be concrete, e.g. Proof(He=
yting,LEM). Without specifying these

constraints I have no id=
ea what a "Proof" means computationally. You

might=
also have to specify further information (ala Lakatos).

=

object? Does it make sense to "multiply" proofs? Clearly you c= an "'and"

At most, I might have a "re=
fute" operation but nothing else leaps to mind.

Tim, the confused CM.

=C2=A0

Hi,

I did a common lisp scri=
pt that dumps the output of the preparsing step in Axiom's compiler. Th=
e preparser is a preprocessing step that takes care of the indentation rule=
s in spad files. In summary, it inserts parentheses and semicolons accordin=
g to the layout.

I'm writing an in=
terpreter for spad files in Lever language to understand how the Axiom envi=
ronment works. The intent is to verify that I've understood how this th=
ing works, and maybe get this CAS embedded into my language.

=

I'm also reading books on category theory, current one in li=
st is the "Category Theory for Computing Science" by Barr and Wel=
ls. If somebody happens to know great books that explain the subject, I wou=
ld like to know.

I already gained several insights=
how I can improve my programming language. I'm probably going to find =
some more as I study deeper into this system.

Henr=
i Tuhola