CODEWITHSUNDEEP
haskell
Pape Sow Traore
Pape Sow Traore

Reputation: 177

number of leaves is one greater than number of nodes in Haskell

I have to prove that given a binary tree, the number of leaves is equal to the number of nodes plus one using induction in Haskell. Given the following type called Tree: 

data Tree = Leaf Int | Node Tree Tree

I defined two functions called leaves and nodes which return the number of leaves and nodes respectively:

With induction, I know that I need to prove the base case which is when the number of nodes is 0 and for the induction step, I need to use the induction hypothesis. But that's throwing me off here is that there are two functions and I don't really know to proceed.In the base case, am I supposed to show that if the number of nodes is 0, the number of leaves is 1 or?

Upvotes: 3

Views: 874

Answers (1)

dfeuer
dfeuer

Reputation: 48591

The tractable way to do this "by induction" is not using induction on natural numbers but rather using structural induction. The proof breaks down like this:

Base case

The base case is for Leaf x, where x is an Int. So you have to prove that for any x

leaves (Leaf x) = 1 + nodes (Leaf x)

Inductive step

In the inductive step, you assume two inductive hypotheses:

  1. leaves t = 1 + nodes t
  2. leaves u = 1 + nodes u

to prove that

leaves (Node t u) = 1 + nodes (Node t u)

I'll let you fill in the actual proofs.

Side note:

Structural induction is a generalization of induction on natural numbers. In particular, you can define the natural numbers as

data Nat = Z | S Nat

You can now do induction with a base case of p Z, and an inductive step that assumes p n and proves p (S n).

Structural induction can itself be generalized further, to well-founded induction, which is the most general mathematical notion of induction of which I am aware. Note that the Wikipedia page is based on a classical notion of well-foundedness; nLab gives a constructive version that is more tightly tied to well-founded induction.

Upvotes: 4

Related Questions