0
$\begingroup$

I'm trying to isolate the key differences between induction and recursion so that I am able to know when to use one over the other.

From my understanding, both can be used to prove properties about recursive structures.

For example:

Consider a recursive structure $x \in X$. In order to prove that for all $x$, $P(x)$ is $true$ one could do this inductively by showing that its $true$ for a base case, then for an inductive case that says if its $true$ for the constituents of a non-base $x$, its $true$ for $x$.

This can also be proved by defining the property $P(x)$ as a function $P:X \xrightarrow{} Bool$ which evaluates to $true$ for every $x$.

Which approach is better in general? I'm leaning towards defining recursive functions as it seems more natural for me as a programmer but maybe its just better here for this specific case, how would one decide what to do in general?

For example lets consider a simple P(x) below. It should be clear to see P(x) is true for all x, given x is an instance of a simple binary tree node.

boolean P(BinaryTreeNode x){ if (x instanceof Leaf){ return true; } else { return P(x.getLeft()) || P(x.getRight()); } }
Improve this question
$\endgroup$
11
  • $\begingroup$ Does this answer your question? $\endgroup$ Commented Sep 13, 2023 at 11:18
  • 2
    $\begingroup$ How does defining the function in the second case prove that the property is true for all $x \in X$? How do you know $P$ evaluates to true for every $x$? How do you know that $P$ is related to the property in question? $\endgroup$ Commented Sep 13, 2023 at 15:22
  • 3
    $\begingroup$ Giving the definition of a recursive function or property does not prove that it always is/returns true. You'd need an inductive proof for that. ("It should be clear that" is not a proof) $\endgroup$ Commented Sep 13, 2023 at 18:55
  • 2
    $\begingroup$ p || q is false if both p and q are false. How do you prove that that ultimately never results in a return false? By induction. $\endgroup$ Commented Sep 13, 2023 at 19:32
  • 1
    $\begingroup$ Incidentally, as someone who works with type theory quite a lot, I'm sympathetic to the idea that there is little difference between induction and recursion. But, there is a difference between a recursive definition of a predicate and an inductive proof that it always holds. The connection is that the latter is a recursive construction of a proof/witness. $\endgroup$ Commented Sep 13, 2023 at 19:40

3 Answers 3

Reset to default
1
$\begingroup$

There seems to be some confusion here. Proof by induction is a valid way to prove facts about recursive structures.

I don't know what you mean by recursion, and the writing in your question doesn't make sense to me. A recursive function is not a proof. Defining a property $P(x)$ or a function is not a proof. I suspect there are some aspects here that you're not explaining well or you haven't fully understood.

In general, recursion is a technique for defining an algorithm, not a technique for proving a statement. See also https://math.stackexchange.com/q/3779213/14578.

Many recursive algorithms can be proven correct by using proof by induction. Perhaps that is what you are thinking of. But there is still an induction proof hidden in there somewhere (even if it hasn't been made explicit).

Improve this answer
$\endgroup$
0
$\begingroup$

Recursive functions and induction are closely related, however Recursive functions do not have to terminate, and a proof using induction does have to terminate, so the induction should include a demonstration of this.

Improve this answer
$\endgroup$
0
$\begingroup$

Here are some predicates/proofs in Agda, a programming language/proof assistant where induction and recursion are essentially the same thing. I can define a type of binary trees like so:

data Tree : Set where leaf : Tree node : Tree -> Tree -> Tree

Then, I can define a boolean predicate that matches yours like this:

P : Tree -> Bool P leaf = true P (node x y) = P x ∨ P y

The ∨ operator is boolean or in the standard library. Now, suppose we tell Agda that 'it should be clear' that this predicate is always true:

P-true : ∀ t → P t ≡ true P-true t = refl

refl being the reflexive proof that $x = x$. Agda rejects this with the message:

P t != true of type Bool

So, to Agda, it is not obvious that that predicate is true for all $t$. The predicate does not just reduce to true for an abstract t. We must prove it by induction:

∨-true-left : ∀{p q} → p ≡ true -> p ∨ q ≡ true ∨-true-left refl = refl P-true : ∀ t → P t ≡ true P-true leaf = refl P-true (node x _) = ∨-true-left (P-true x)

As you can see, this proof by induction looks just like the recursive definition of the predicate. But, the recursive definition of the predicate is not sufficient to establish the universal truth of the predicate. The proof by induction recursively constructs a proof that the predicate is always true. This isn't particularly difficult, and the structure of the inductive proof closely follows the structure of the predicate's definition, which is why you probably consider it "clear." But giving the full details requires actually making this argument.

This structure is not much different than a full-fledged predicate in Agda, which looks like this:

P : Tree -> Set P leaf = ⊤ P (node x y) = P x ⊎ P y all-P : ∀ t → P t all-P leaf = tt all-P (node x _) = inj₁ (all-P x)

⊤ is the trivially 'true' type, and ⊎ is disjoint union, which is 'true' (has a value) if either of its sides is 'true'. The proof that the predicate holds for all $t$ has exactly the same structure as the boolean version.

There are occasionally reasons to prefer one of these sorts of definitions in Agda (or others that are roughly equivalent). But they have to do with technical details about how Agda behaves. In general they are largely the same.

Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.