Lecture 29: Functions vs. Relations

1 Purpose

Explore functions vs. relations.

2 Outline

You’ve written many functions in your programming career, and a bunch in this class. You’ve also now seen quite a few "relations" in this class, which often capture similar ideas. e.g., we had an even function:

def even : Nat -> Bool
| 0 =>  true
| 1 => false
| Nat.succ (Nat.succ n) => even n

And an even relation (we had another as well, but we’ll get to that):

inductive ev : Nat -> Prop where
| O : ev 0
| SS (n : Nat) (H : ev n) : ev (Nat.succ (Nat.succ n))

We talked (and proved) that the two were equivalent by showing that if you had one you could get the other, e.g., proved the following theorem:

theorem even_ev : forall n, even n = true <-> ev n := by sorry

But how are they different, and how are they the same? That is the purpose of this lecture.

3 Functions

First, we need to be more formal about what a function is. Mathematically (and the functions in Lean are mathematical functions, i.e., given the same input, they always return the same output), a function is a mapping from inputs to outputs. Another way of stating that is that it is a (potentially infinite) set of input-output pairs, with the restriction that for any input, there is only one output (as calling a function on a particular input can only give you one output).

e.g., we could characterize even as:

Where we would have to give infinite pairs.

We can do this for any finction. For example, the factorial function:

def factorial : Nat -> Nat 
| 0 => 1
| Nat.succ n => (Nat.succ n) * factorial n

Could also be defined as:

4 Relations

So what is a relation? A relation is a generalization of a function, in that it does not have the restriction that there is only a single output for a given input. Instead, it is a set of niput-output pairs, where there can be multiple outputs for a given input. So any function is as relation, but some relations are not functions. More concisely, you can think of a relation as a connection between inputs and outputs. One way you might get to a relation is by defining a function, and then making the function nondeterministic, i.e., allow it to potentially return different outputs for the same input.

How can we represent relations? Well, in any language we can represent a relation as a predicate (boolean returning function) on pairs (of input-output). e.g., a relation for even could be:

def even_rel : Nat × Bool -> Bool 
| (n, true) => n % 2 == 0
| (n, false) => n % 2 == 1

Or we could represent the factorial relation as:

def factorial_rel : Nat × Nat -> Bool 
| (n, m) => factorial n == m

The latter being a bit circular, but a valid definition.

But in Lean, we have another way of representing relation that turns out to be really useful when we are writing proofs. Rather than writing them as functions that take pairs and return booleans, we can define them as inductive types.

This is useful because if we are trying to prove something about, e.g., the factorial function, if we have the function, all we know is the input and output: the structure of the code is opaque. But if we represent it as an relation, and encode that as an inductive type, then the structure of the computation corresponds to the constructors of the indpuctive type. We can do case analysis, induction, etc. We’ve seen the ev relation many times, so let’s do one for factorial instead:

inductive fact : Nat -> Nat -> Prop where
| O : fact 0 1
| S (n m : Nat) (H : fact n m) : fact (Nat.succ n) ((Nat.succ n) * m)

Now, why does that relation mean the same thing? And in general, why does this approach work? Rather than proving it (which we’ll do later), let’s look at how the factorial function evaluates. e.g., factorial 4:

factorial 4 =
4 * factorial 3 =
4 * (3 * factorial 2) =
4 * (3 * (2 * factorial 1)) =
4 * (3 * (2 * 1 * factorial 0)) =
4 * (3 * (2 * 1 * 1)) = 24

Now, we know this, and we can confirm that we got from the beginning to the end by running #eval factorial 4, but if we are trying to prove something about the factorial function, e.g., we have a hypotheses factorial n = m, there is no way to extract that structure from the hypothesis.

Now, let’s look at the same thing, but with the relation. In this case, we want to see how a value of type fact 4 24 is constructured: i.e., how we construct a proof that the pair (4, 24) is in the factorial relation.

#check (fact.S 3 _ (fact.S 2 _ (fact.S 1 _ (fact.S 0 _ fact.O))) : fact 4 24)

We can see that the term is a sequence of constructors, each of which is a step in the computation: the same steps as we see above when we wrote out how factorial evaluated, but unlike something on paper, this is an actual value we can use in our proofs.

To see this, and to see how this structure can be useful in our proofs, lets show that the two representations are equivalent. One direction (going from the inductive) ends up being easier, because the inductive relation contains so much more structure we can make use of in our proof:

theorem fact_factorial : forall n m, fact n m <-> factorial n = m :=
 by intros n m
    apply Iff.intro
    case mp =>
      intros H
      induction H <;> simp only [factorial, *]
    case mpr =>
      intros H
      revert m
      induction n <;> intros m H
      case zero =>
        simp only [factorial] at H
        rw [<- H]
        constructor
      case succ n IH =>
        simp only [factorial] at H
        rw [<- H]
        constructor
        apply IH
        rfl