[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
So, you're probably on your way to new understanding. But, I thought I'd present a couple quibbles with the way you described your understanding of induction, in case they could help when reading the papers and whatnot. First, your description of induction on the naturals sounds like a procedure for enumerating proofs for every possible value. If this is indeed, the intention, I don't think it even requires ordinals to break down. For instance, consider arguing that the length function on lists is justified. Unless you can enumerate the type of the _elements_ of the list, there is no way to enumerate all lists. You can't enumerate all the lists of real numbers. So it seems like any tying of induction to enumeration of the underlying type is doomed to failure. Rather, the claim of (forall n. P n) is that for any choice of n, we can calculate a proof P n. In type theories, this works exactly like recursive definitions are expected to work. Inspect n. If it's 0, use the base case. If it's 1+m, make a recursive call with m, and apply the successor case. The other quibble is why you believe (forall n. P n) is justified, even given your description. Yes, for finite n, we can accomplish this procedure in finite time. Presumably this means that you believe all natural numbers are finite. This presumably means you also believe that there is a lack of ability to construct self-referential values, so that for instance m in my above description is 'smaller' than n. But this is the same reasoning behind well-founded trees (ordinals, your ty type, ...). There is no ability to construct self-referential trees, so the function that you get from t = Mk f must produce smaller trees than o itself. And recursion consuming any particular well-founded tree takes finite time, so (forall t. P t) is justified. For instance, copying the finite naturals into ty is a function producing all finite values: embed : nat -> ty embed 0 = Ax embed (S n) = Suc (embed n) Of course, the apparent self-reference in embed is really sugar for recursion on the natural numbers. All the values produced by `embed` are lesser than `Mk embed`, and the idea is that the system is constructed so that this is always the case. Any `Mk f` was necessarily produced by defining f to produce values that cannot include `Mk f` themselves. The other piece is a generalization of your function. When you see `Mk x`, you call x with 2. So, even though `Mk embed` cannot exactly be given any finite height, because embed produces arbitrarily large values, you only request the one with size 2. The generalization is that when we proceed recursively by applying: lim : (forall n. P (x n)) -> P (Mk x) the argument is simply bundling up the recursive call as a function, and lim is only capable of calling it at finitely many values of finite size. So the trace of constructing the proof of `P (Mk x)` only proceeds down finitely many of the infinite choices of branches, and each of those branches are well-founded, and take finite time to complete, by hypothesis. (This probably gets a little more complicated if P itself is like a function, so it can choose how many branches to use based on an argument; but then for each choice of argument, a finite number of branches is followed, and it doesn't take infinite time to 'construct' a function just because the domain is infinite.) Trusting/proving these properties of the system isn't trivial, but it must be done to justify even induction on the natural numbers. It may be a bit harder to see why you should trust them for more complicated well-founded trees, but the arguments are kind of fundamentally the same. Cheers, Dan On Sat, Jan 13, 2018 at 8:18 PM, Richard Eisenberg <r...@cs.brynmawr.edu> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Many, many thanks to all who provided responses, several of which were > off-list. I thought I'd summarize the bulk of responses. > > What I did not explain in my original email -- but bears importance in how > this all fits together -- is my mental model of induction. For a natural > number induction of a proposition P : Nat -> Prop, we can imagine that, for > any n, we can eventually build up a proof of P(n). We do this by starting > by proving P(0), using that to prove P(1), using that (perhaps both of > those) to prove P(2), and so on. After n+1 steps, we'll prove P(n). Thus, > we can prove P(n) in finite time, for any finite n. Accordingly, we can > conclude (forall n, P(n)). > > However, this approach -- prove a proposition by building up a finite > number of sub-proofs -- fails for my `ty`, below. (This `ty` is, by sheer > coincidence, a representation of the ordinals, as used in, e.g., Abel and > Altenkirch's http://www.cse.chalmers.se/~abela/foetuswf.pdf < > http://www.cse.chalmers.se/~abela/foetuswf.pdf>) It would take an > unbounded number of sub-proofs in order to prove a proposition over a `ty` > made with `Mk`. > > The insight I gained from the answers is that it's OK to require this > unbounded number of sub-proofs. Equivalently, it might take an infinite > amount of time to prove a proposition, but that doesn't cause trouble. The > well-foundedness of this approach, called transfinite induction, is proved > in Abel and Altenkirch's paper, above. I have not tried to digest it, but I > trust the result. Indeed, some responses have pointed out that because > structural induction is equivalent in power to transfinite induction, it > might be easier to teach the latter by reference to the former. > > Dybjer (http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf < > http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf>) also > gives a thorough treatment of inductive types. Having been satisfied by the > Abel and Altenkirch paper, I have not dived into the details here, but it > seems to address my concern, as well. > > Another intriguing answer is that some aspect of mathematics is, and > always will be, an article of faith. We can use the edifice of mathematics > built up from, say, set theory to prove the well-foundedness of transfinite > induction. Or, if we use type theory as the basis for mathematics, > structural induction is taken as a given. Either way, we're basing our > result on unprovable axioms. > > Once again, thanks to all. I've learned a new nugget of knowledge through > this interaction! > Richard > > > On Jan 6, 2018, at 5:23 PM, Richard Eisenberg <r...@cs.brynmawr.edu> > wrote: > > > > [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > > > > Does anyone know a place I could see a statement of how structural > induction works, spelled out in full detail? I don't need a "canonical" > (i.e. citable) reference, per se, but a place I can enhance my own > understanding of structural induction. > > > > My problem is that I had been blithely assuming that structural > induction was reducible to natural-number induction, where the natural > number was the size (number of nodes in the tree) of the structure. But > this is clearly not true, as both Coq and Agda accept this (written in Coq > notation): > > > > Inductive ty := > > | Ax : ty > > | Suc : ty -> ty > > | Mk : (nat -> ty) -> ty. > > > > Fixpoint f (t : ty) : nat := > > match t with > > | Ax => 1 > > | Suc t' => 1 + f t' > > | Mk x => 1 + (f (x 2)) > > end. > > > > Note that there's no good way (that I see) of denoting the size of such > a structure. And yet, Coq feels confident that my f will terminate. Indeed, > I certainly don't have a counterexample to this, and I don't believe there > is one. > > > > So, I'm looking for a description of structural induction that explains > how the function above is terminating in a rigorous way. Bonus points if it > also shows how non-strictly-positive recursive occurrences of a type in its > own definition cause structural induction to fail. > > > > Thanks! > > Richard > > > > -=-=-=-=-=-=-=-=-=-=- > > Richard A. Eisenberg, PhD > > Asst. Prof. of Computer Science > > Bryn Mawr College > > Bryn Mawr, PA, USA > > cs.brynmawr.edu/~rae <http://cs.brynmawr.edu/~rae> > >