Is it possible to define binary trees without a new inductive type?

Using Coq
1

Binary trees (without any attached data) can be encoded in Coq as the following inductive type:

Inductive bin :=
| Leaf : bin
| Node : bin -> bin -> bin.

Given just the basic types of Coq (dependent functions, unit, sums, products, equality, dependent pairs) as well as the natural numbers, and their respective induction rules, is it possible to encode the type bin without defining a new inductive type? In particular, can this encoding be defined so that the appropriate induction rule is provable:

bin_rect
     : forall P : bin -> Type,
       P Leaf ->
       (forall a b : bin, P a -> P b -> P (Node a b)) ->
       forall b : bin, P b

More generally, I’m wondering if induction on natural numbers is sufficient to encode more complicated/branched forms of induction such as binary trees, or if it is necessary to add general inductive types/W-types to the theory.

Thanks!
-Raffa

2

I’m glad you’re interested in this topic; it is one of my favorite areas of study.

Since the type of binary trees is countable, they are in bijection with the natural numbers, and can be defined as such. Letting pair (x y : nat) : nat := 1/2 (x + y) (x + y + 1) + y be the Cantor pairing function, we can define Leaf := 0 and Node x y := 1 + pair x y.

Since pair is invertible, the induction principle will be provable, though it will only satisfy the expected computation rules/equations up to propositional equality, not definitional equality.

I believe tricks like this work for all finitary types (if they carry data, you can define the skeleton, and then use large eliminations and dependent pairs to stick the data on afterwards), but once you have infinitary inductive arguments (ex. a constructor of type (nat -> bin) -> bin you need at least W-types.

W-types with large eliminations plus dependent pairs (with definitional eta) and equality (with J that computes on refl) are enough to construct most all inductive types with induction principles with definitional computation rules, though the encoding is rather complex.

This includes uniform parameters of any size, mutual inductives in the same predicative sort (Prop messes things up here), small non-uniform parameters, and small induction-recursion.

Inductive types which I don’t believe any encoding just using W-types can have definitional computation rules include constructors like list bin -> bin, or types with a large, non-uniform parameter. These types can however be constructed with propositional computation rules.

Inductive-inductive types probably require function extensionality or UIP to get even propositional computation rules.

Large induction recursion and higher inductive types definitely require strict extensions of the theory.

Everything I’ve said here is mostly about inductives in Set or Type. Inductives in Prop may behave slightly differently.

1 Like