Luke Palmer luqui

In this document I attempt to build some intuition for the ordinals by constructing several concrete well-orderings of the naturals with order types up to (and including!) epsilon 0.

Ordinals are all about well-orderings. A well ordering of the naturals is an ordering -- call it <~ -- on the naturals that has no infinitely descending chains. So the reverse ordering, x <~ y iff y < x, is obviously not a well-ordering because it has the infinitely descending chain 1 ~> 2 ~> 3 ~> ....

However, the usual ordering is a well-ordering, because if you start at n, you only get at most n steps before you have to hit 0. The usual ordering is called "omega", which I denote w.

Let [ ] : Ord -> Relation Nat be a function that realizes an ordinal into a well-ordering of the naturals with that order type.

Given a relation R on the naturals, we define the restricted relation R(<n) to be R but just acting on the first n naturals.

Defn: [ ] is continuous iff for every series of ordinals a_i whose limit is l, for every natural n, there exists an i such that for all j > i, [a_i](<n) = [l](<n).

Intuitively, if you are only looking at a finite prefix of the naturals, you can get to a limit ordinal by going finitely high up its limit sequence.

Daniel Spiewak's [proof][1] that there exist total functions which are not inductive uses the following assumption:

I am going to assume that the problem of determining whether some arbitrary function is inductive [...] is in fact decidable. I actually don't have a reference on this one, but it seems like a fairly reasonable assumption. Formally:
exists D, forall f, f in I <=> (D(f) = TRUE)

I have modified the statement of the assumption slightly. In fact, my modification is not equivalent to the original, since my version says "there is a decider for inductive functions" where the original is "there is a single decider for both inductive and coinductive functions". It is conceivable that there is only a technique that can tell whether a function was either inductive or coinductive but can't tell which it is, in which case the above statement would not be implied. But that is an exotic enough possibility that I'm comfortable with my simplification.

However, the statement of the assumption

Maybe if I keep rewriting this document I will eventually stumble on what I want.

Goals:

Support for programming environment with ever-increasing social vocabulary (i.e. 'helper' functions become global vocab words).
"Type system" whose primary purpose is to document the meanings/usages of words.

The way I have been picturing (2) is by allowing types to be fabricated into existence without a formal (or representational) definition. For example, if we wanted to talk about primes as a type, we could, but we wouldn't have to describe to the computer what it means to be prime. It is human communication. So:

-- inverse p n finds the multiplicative inverse of n mod p.

Going a bit crazy here... I want to make some language-design art, but I can't decide on what to do.
There's propdoc, interactive coding environment (ice?), new ideas floating around wrt syntax and focus. I just want to do something!

Ok, more thinking then, there needs to be a focus to the excitement, and I can't make a good ice without a type system, and existing type systems are too intensional for it. Auto-abstraction might be too lofty a goal, that could be what is constraining me. And yet, it is sortof essential to the idea. Well, there is really only one problem with it, and that is the lexicon distinction I have been talking about. But that is a modularity problem; module systems need to be the most perfect, they are the outermost part of your code, they almost touch the cold outside air.

x :Y is shorthand for x [Y 'x].

Definition of functions:

A B :*
->
function :*
(f :function x :A -> apply :B)   -- application
((x :A -> y :B) ->               -- abstraction

f :function

Sequent was coming along sortof nicely, but I am reminded of the enamoring simplicity of Lisp. It was the first functional language (right?), because it could be implemented before anybody knew how to program functionally. That is also the source of some of its warts, but all in all it was a great start. My question: is there a simple meta-circular definition of a knowledge-oriented language like the one I am trying to build? Maybe if I can find something small and essential, it will allow me to explore the programming space with it without getting lost in implementation details.

I think tactics may be the key. I have always thought of tactics as a layer above the core proof engine (which is good for verifiability), but maybe an essential kernel takes tactics more seriously, and the core logic less seriously.

Here is a potential guiding principle: you have knowledge, and with tactics you manipulate it. The first place my mind goes is to higher-order tactics, essentially interacting with knowledge th

	sq = floor . sqrt . fromIntegral

	primes = 2:filter (\n -> all (\m -> not (m `divides` n)) (cand n)) [3..]
	where cand n = takeWhile (<= sq n) primes

	m `divides` n = n `mod` m == 0

	fibs = 0:1:zipWith (+) fibs (tail fibs)

	l5 p \| p5 == 1 \|\| p5 == 4 = 1

	mergeEq :: (a -> a -> Ordering) -> [a] -> [a] -> [(a,a)]
	mergeEq cmp (x:xs) (y:ys) =
	case cmp x y of
	EQ -> (x,y) : mergeEq cmp xs ys
	LT -> mergeEq cmp xs (y:ys)
	GT -> mergeEq cmp (x:xs) ys
	mergeEq f _ _ = []

	Set Implicit Arguments.

	Require Import List.

	Inductive Vec A : nat -> Type :=
	\| nilV : Vec A O
	\| consV : forall n, A -> Vec A n -> Vec A (S n).

	Inductive T : nat -> Type :=
	\| Var : T 1