Martin,
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 know if this research has come to
>any conclusions on these issues?
Not to my knowledge.
Tim
[0] Loizeau, Nicolas "Building A Computer In Conway's Game Of Life:
[1] Goucher, Adam "Spartan Universal Computer-Constructor"
[2] Rendell, Paul "A Turing Machine In Conway's Game Of Life"
[3] Nagel, Ernest and Newman, James R. "Godel's Proof"
New York University Press (2001) ISBN 0-8147-5816-9
[4] Goldstein, Rebecca "Incompleteness -- The Proof and Paradox of Kurt Godel"
W.W. Norton (2005) ISBN 0-393-32760-4
[5] Shankar, N. "Metamathematics, Machines, And Godel's Proof"
Cambridge University Press (1994) ISBN 0-521-58533-3
A man's reach should exceed his grasp, or "what the safety harness is for" -- daly