Re: Axiom musings ... runtime computation of first-class dependent types

[Martin Baker]

Tim,

Thanks for your reply, lots to think about in this subject isn't there.
Like you I'm attempting the daunting (but interesting) path of trying to 
understand this subject better.



Dependent types allow functions to exist in the type definition. The
functions can be executed "at run time". Current languages that have
support for dependent types such as Agda and Idris use very, very
limited forms of this facility. They only extend the type in certain
carefully defined ways that allow the compiler to type check the code.


Yes, as you say, natural numbers (and related structures such as lists) 
have very nice properties. Idris does a good job of seamlessly 
converting between the Peano form (for proofs) and the usual form (for 
efficient algebra).


I like this idea that the representation holds the full information 
about the domain so its fully defined for proofs as well as holding the 
data for algebra.


As a thought experiment, I am trying to work out what it would take for 
this to be done on all mathematical structures.


As a first step, could this be extended to integers?

We could say that Integer = Nat+Nat. In spad terms that would be:
Rep := Union(negative : NNI, positive NNI)

Or Integer = 2*Nat. In spad terms that would be:
Rep := Record(sign : Bool, value NNI)

This would provide a structure to store an integer so it would work for 
the algebra but it doesn't seem to fully define an integer for proofs in 
that it doesn't glue the negative and positive Nats together. For that 
we seem to need equations like:


S (-1) = 0
P 0 = -1
S P = P S = Id

where:
S is successor
P is predecessor

As soon as we add equations to the representation then we loose some of 
the nice properties - more complexity - no canonical form.


At each step we seem to loose nice properties, when we get to fraction:

Rep:= Record(num:IntegralDomain, den:IntegralDomain)

Then we seem to need to need a normalisation algorithm to put in normal 
form so we can test for equality.


I still think there is something very powerful about combining algebra 
and proofs in this way so I would be interested to know if you have 
found a path through all this?


Martin

Re: Axiom musings ... runtime computation of first-class dependent types

[Tim Daly]

Martin,

>In this series of videos Robert Harper gives an provocative take on
>these subjects:
>https://www.youtube.com/watch?v=LE0SSLizYUI


I watched Harper's videos years ago. I will revisit them. If you haven't
seen them I highly recommend them. Indeed, the whole series of
lectures from professors at OPLSS is well worth the time.



>At about 37 min into this video  he says: "what is true has unbounded
>quantifier complexity whereas any formalism is always relentlessly
>recursively innumerable" - Gödels theorem.

Yes, in general, the quantifier complexity is unbounded. But for a given
particular case it is not. Can a system always shape itself to the
particular
problem using only bounded quantifiers?

I previously made an argument that while Godel used self-reference
he did not use self-modification. I conjectured that self-modification could
weaken his conclusion. The response was that self-modification could
be modeled in a type system and would have no effect.

I'm still unconvinced but that's the conclusion from people who study types
for a
living so I'm almost certainly wrong.

The topic is still open in my mind and I'm spending a bit of time reading
everything I can about the Godel proof. [3,4,5] Self modifying code
involves time.
I need to study time-related type theory.

There is also the question of embedding self-modifying code in some
Godel-like numbering system (or something equally clever I'm probably
not capable of inventing).

My current thinking is to find some way to write Godel's proof in a
"Game of Life" automata. There are whole computers that have been
embedded in these systems. If I could embed Godel and a computer in the
same space with some clever encoding I'd have a way of executing programs
that reference themselves. [0,1,2]




>Do you think that dynamic types and/or the sort of self modifying
>programs you are suggesting are necessary to model all of mathematics?

A model of all of mathematics seems to be the goal of homotopy
type theory. Despite numerous online courses and various readings
it is still beyond my understanding.

Dependent types allow functions to exist in the type definition. The
functions can be executed "at run time". Current languages that have
support for dependent types such as Agda and Idris use very, very
limited forms of this facility. They only extend the type in certain
carefully defined ways that allow the compiler to type check the code.

These "bottom up" limited extensions will never reach high enough to
type check Axiom code. One of the reasons is the artificial split between
compile-time and run-time. What the compiler can't type check in general,
the runtime can type check in particular.

I think that type erasure is one of the goals but Axiom carries types
all the time and can create new types "on the fly" so type erasure
is a non-issue for me. I'm not even sure that type erasure is meaningful
in a dependent type system where types are first-class.

I'm merging the compiler-interpreter into a single thing, trying to do as
much type checking as possible at any point, some of which has to be
pushed to the last instant.

Further, I'm able to invoke the entire system (it is all in Lisp) as "the
function"
evident in some type declarations. The call gives Lisp the type being
defined,
the program being typed, and the entire environment containing definitions
and axioms.

In order for this to work at all the various Axiom functions need really
good
specifications. The specifications focus the proof search. For instance, GCD
is a triple case test such as

Given x:Nat and y:Nat and updated copies x' and y' repeat case
(x > y) and (x' = x - y) and (y' = y)
(y > x) and (y' = y - x) and (x' = x)
(x = y) done

we now have essentially a state machine with monotonically decreasing
values. Note that there are about 20 domain specific GCD algorithms in
Axiom, such as the polynomial GCD. Is there a general specification for all
of
the algorithms or are additional definitions needed in scope? That's
still to be researched. Is there a way to "factor" the specifications?
Again,
another research question I can't yet answer.

In Axiom-speak, NAT is NonNegativeInteger. Axiom conflates the data
structure, known in logic as the carrier, with the domain, known in logic
as the type. In SANE the data structure and domain are separate so it
should be possible to write specifications over multiple "carriers".

Another item on the "ponder list" is how to dynamically construct CLOS
types that carry the definitions, axioms, and type structure. I'm still at
the
stage of embedding LEAN axioms into a hierarchy similar to the existing
Axiom hierarchy.

As for modeling all of mathematics my goal is only on computer algebra.
Rumor has it that programs are proofs. If that's assumed I have
several hundred programs (proofs) in Axiom. I'm trying to unify the programs
with their more formal proofs.


>These videos are 4 years old, do you 

Re: Axiom musings ... runtime computation of first-class dependent types

[Martin Baker]

Tim

In this series of videos Robert Harper gives an provocative take on 
these subjects:

https://www.youtube.com/watch?v=LE0SSLizYUI

At about 37 min into this video  he says: "what is true has unbounded 
quantifier complexity whereas any formalism is always relentlessly 
recursively innumerable" - Gödels theorem.


"there is a distinction between proof and truth"
(by formalism here I think he means formal logic?)

It looks to be like the programming style he is putting forward is 
dynamic typing? I cant find it now, in these videos, but I think he 
might have suggested that this style of programming is required to model 
all of mathematics (be foundational)? Even cubical type theory might not 
be foundational?


Do you think that dynamic types and/or the sort of self modifying 
programs you are suggesting are necessary to model all of mathematics?


These videos are 4 years old, do you know if this research has come to 
any conclusions on these issues?


MJB

On 29/05/2022 08:50, Tim Daly wrote:

Well, SANE is certainly turning into a journey.

When we look at the idea of first-class dependent types
as implemented in languages like Agda and Idris we find
what I call "peano types". For example, Fin is a type
of "finite numbers", usually defined as

data Fin : Nat -> Type where
   FZ : Fin (S n)             -- the base case
   FS : Fin n -> Fin (S n)    -- the recursive case

Fin 7 describes 7 numbers 0..6

This construction is popular because the compiler can
compute that the type construct is total. Thus the
type construct is its own proof.

A dependent type allows computation to occur during
its construction. The canonical example is defining
a list of length m, which depends on the value of m.
Another list of length n is a separate type. An
append function of these lists computes a new typed
list of length (m + n).

The current approach, Agda, Idris, etc., is "bottom up"
where restrictions are placed which will allow proofs
in all contexts.

There are excellent reasons for such carefully
styled dependent types.

Reading the literature you come across the famous
Dan Friedman admonition "Recursion is not allowed",
usually in reference to his Pie language [0]. While
Pie does not allow it, he admits 2 kinds of recursion
(pp 358-359).

The general case of first-class dependent types I'm
considering is capable of much broader and more
ill-founded behavior. This is deliberate because some
of the mathematics in Axiom can only be proven correct
under limited cases. These cases have to be constructed
"on the fly" from more general dependent type definitions.

For example, a type might not be total in general but
it may be possible to compute a bounded version of the
type when used in context. This can only be decided at
run time with the given parameters in the given context.
In general, this means computing that "in this context
with these bindings the result can be proven".

This general case occurs because a SANE type G is able to
invoke all of lisp with an environment that contains the
type G under construction as well as its environment
which contains the program. This allows the type G to self
reference and self modify based on context.

The general type G:List(G,REPL) in a context of a statement
M:G := (append '(1 2 3) '(4 5 6 7)) as effectively typed
M:List(7).

The SANE type G is neither sound nor complete but List(7) is.
The game is to construct a contextually dependent type and
the associated proof "on the fly".

An intuitive Gedankenexperiment is defining an arm for a
general robot. One could have a 2 arm robot defined as
Robot : TwoArm(Robot,Repl).

The problem, based on context, might generate each of the
two arms separately, one with 7 degress of freedom to
reach the whole of the workspace (in context) and a second
4 degree robot that can position and hold a part in the
reach of the first arm. The same TwoArm type might resolve
to a different configuration in a different context.

Self-reference is already a metamathematical problem
(witness Godel's proof). Self-modification is, as Monty
Python famously says, "right out". One might argue with
Godel but contradicting Python is heresy.

The SANE game is to create the general case of first-class
dependent types with such abilities and then find certain
restrictions as necessary to try to construct the proof
in a given context. This SOUNDs COMPLETEly crazy, of course.

One has to construct a lisp program "on the fly" in the
dependent type context, prove it correct, and return the
new type with the type-program and proof. Values, during the
run time computation may have to be dynamically substituted
in the type-program, re-running the proof with those values.

At best this ranges from the nearly impossible to horribly
inefficient. We all know this can never work.

This seems necessary as Axiom's computer algebra algorithms
were never developed with proof in mind. It seems necessary
to start "from the top" and work downward to the instance
of 

Axiom musings ... runtime computation of first-class dependent types

[Tim Daly]

Well, SANE is certainly turning into a journey.

When we look at the idea of first-class dependent types
as implemented in languages like Agda and Idris we find
what I call "peano types". For example, Fin is a type
of "finite numbers", usually defined as

data Fin : Nat -> Type where
  FZ : Fin (S n) -- the base case
  FS : Fin n -> Fin (S n)-- the recursive case

Fin 7 describes 7 numbers 0..6

This construction is popular because the compiler can
compute that the type construct is total. Thus the
type construct is its own proof.

A dependent type allows computation to occur during
its construction. The canonical example is defining
a list of length m, which depends on the value of m.
Another list of length n is a separate type. An
append function of these lists computes a new typed
list of length (m + n).

The current approach, Agda, Idris, etc., is "bottom up"
where restrictions are placed which will allow proofs
in all contexts.

There are excellent reasons for such carefully
styled dependent types.

Reading the literature you come across the famous
Dan Friedman admonition "Recursion is not allowed",
usually in reference to his Pie language [0]. While
Pie does not allow it, he admits 2 kinds of recursion
(pp 358-359).

The general case of first-class dependent types I'm
considering is capable of much broader and more
ill-founded behavior. This is deliberate because some
of the mathematics in Axiom can only be proven correct
under limited cases. These cases have to be constructed
"on the fly" from more general dependent type definitions.

For example, a type might not be total in general but
it may be possible to compute a bounded version of the
type when used in context. This can only be decided at
run time with the given parameters in the given context.
In general, this means computing that "in this context
with these bindings the result can be proven".

This general case occurs because a SANE type G is able to
invoke all of lisp with an environment that contains the
type G under construction as well as its environment
which contains the program. This allows the type G to self
reference and self modify based on context.

The general type G:List(G,REPL) in a context of a statement
M:G := (append '(1 2 3) '(4 5 6 7)) as effectively typed
M:List(7).

The SANE type G is neither sound nor complete but List(7) is.
The game is to construct a contextually dependent type and
the associated proof "on the fly".

An intuitive Gedankenexperiment is defining an arm for a
general robot. One could have a 2 arm robot defined as
Robot : TwoArm(Robot,Repl).

The problem, based on context, might generate each of the
two arms separately, one with 7 degress of freedom to
reach the whole of the workspace (in context) and a second
4 degree robot that can position and hold a part in the
reach of the first arm. The same TwoArm type might resolve
to a different configuration in a different context.

Self-reference is already a metamathematical problem
(witness Godel's proof). Self-modification is, as Monty
Python famously says, "right out". One might argue with
Godel but contradicting Python is heresy.

The SANE game is to create the general case of first-class
dependent types with such abilities and then find certain
restrictions as necessary to try to construct the proof
in a given context. This SOUNDs COMPLETEly crazy, of course.

One has to construct a lisp program "on the fly" in the
dependent type context, prove it correct, and return the
new type with the type-program and proof. Values, during the
run time computation may have to be dynamically substituted
in the type-program, re-running the proof with those values.

At best this ranges from the nearly impossible to horribly
inefficient. We all know this can never work.

This seems necessary as Axiom's computer algebra algorithms
were never developed with proof in mind. It seems necessary
to start "from the top" and work downward to the instance
of existing code, adding restrictive assumptions as needed.

The moral of the story is "Never give a lisper a REPL".

There are some who call me ... Tim [1]




Amusing historical note: Code linters were discovered during an
omphaloskepsis session.

[0] Friedman, Daniel P. and Christiansen, David Thrane
"The Little Typer", MIT Press (2018) ISBN 978-0-262-53643-1

[1] https://www.youtube.com/watch?v=co3ygE6H7PU