[TYPES] Statement of structural induction

[Dan Doel]

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 <rae at 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 <rae at 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>
>
>