Do people talk about "inductive definitions"? I mostly only hear about induction in the context of proofs, in which case I'd say that an inductive proof/argument is one that uses the recursive structure of whatever it's about.

A recursive definition is: "natural numbers are 0 or a natural number + 1". An (abridged) inductive proof that uses the recursive nature of natural numbers: "the sum of all naturals up to n is n(n+1)/2: 0*(0+1)/2 = 0, and (n+1) + n(n+1)/2 = (2(n+1) + n(n+1))/2 = (2n + 2 + n^2 + n)/2 = (n^2 + 3n + 2)/2 = (n+1)(n+2)/2 = (n+1)((n+1)+1)/2"

> A recursive definition is: "natural numbers are 0 or a natural number + 1".

Note that this isn't enough by itself to support proof by induction.

Consider the definition of a list in Haskell which is analogous to the above definition of natural numbers: "lists are [] or a list with an element prepended".

Infinite lists satisfy this definition.

But how do you know that induction is valid to use on natural numbers? It's because their definition/construction follows a set of rules that makes them inductive. Some languages like Coq make this explicit by providing an 'Inductive' keyword for defining inductive types.

I think the closest short answer is that recursive definitions are just a special case of inductive ones for writing functions.

If you've looked at recursive functions then you should also look at recursive functions.

The jargon file entry for "tail recursion" read: "If you haven't grown tired of it already, see tail recursion."

To not understand recursion, you must first... wait, I think that's all!

Iteration is just recursion over a list/array/generator.

I don't know if that's a helpful framing?

    def sum(arr):
       total = 0
       for x in arr:
          total += x
       return total

and

    def sum(arr):
      if len(arr) == 0:
         return 0
      return arr[0] + sum(arr[1:])

both operate over an array but I'd call one of them recursive and the other iterative.