Lecture 13: Functions

1 Purpose

Explore termination of functions in Lean.

2 Outline

And as we have seen, there are often many different ways of implementing the same function, some of which Lean cannot figure out how terminate. When we get to proving, this will be very important, but if you just wanted to use Lean as a programming language, you could either declare the function as partial (which means that it may not terminate), or you could leave an unproved decreasing_by argument.

def even (n : Nat) := n % 2 = 0

def even' : Nat -> Bool
  | 0 => true
  | 1 => false
  | n + 2 => even' n

def even'' (n : Nat) := match n with
  | 0 => true
  | 1 => false
  | n + 2 => even'' n

partial def even''' (n : Nat) := 
  if n = 0 then true
  else if n = 1 then false
  else even''' (n - 2)

def even'''' (n : Nat) := 
  if n = 0 then true
  else if n = 1 then false
  else even'''' (n - 2)
decreasing_by sorry

Termination If you recall from last time, typechecking the term, to confirm that it has the type, is all that we need to do to confirm that the theorem has been proved. The typechecker is what protects our notion of provability. If we were able to typecheck terms that have false types, this woul be very bad. For the theorem to be valid, it is sufficient that there is some way of getting from the arguments to the conclusion, which the typechecker will confirm: any details that are finer than captured by the type (i.e., the theorem) are not what we were proving, and thus aren’t relevant for the perspective of proving the theorem. This is a very different situation from most type systems, where there are many important details that are not able to be captured by the type, and thus the idea that merely having an implementation would be sufficient would seem ludicrous.

This has an important consequence: all functions must terminate. This is because if you could write a function that did not terminate, you could quite easily write a nonsense proof. For example:

def T_helper (x : Bool) : true = false := T_helper true
decreasing_by sorry

theorem T : true = false := T_helper true

This seems absurd, but you can do it in, e.g., Haskell, and it’s why Haskell’s type system isn’t suitable for logical reasoning, since any type is inhabitable (so if types are theorems, any are provable, even false ones!).

Technically, this means that definitions (and theorems) in Lean need to be total. Now, Lean does allow you to write partial functions if you need them, by writing partial def. We won’t use this in this class, but if you are thinking of using Lean more generally, it is a general purpose programming language that also has a first class theorem prover built-in. Partial definitions cannot be proofs, but they can be useful for programs!

How does Lean check that a function is total? As you might know, there is no way of taking a general program and determining if it is going to terminate: this is one of the most famous results in all of computer science. What you can do, on the other hand, is construct proofs that a particular program is going to terminate. Lean can do this automatically if you write programs in a certain form, and also allows you to provide proofs in the case that it can’t do it automatically. We’ll spend most of our time constructing our functions in such a way as to allow Lean to do this for us automatically, though we will cover how to handle the more tricky cases.

At this point, everything, aside from termination, is typical for a typed functional language (and indeed, we haven’t covered how to define new types, among other important features). How else does Lean differ? Well, we said that everything has a type, and that includes types:

#check Nat               -- Type
#check Bool              -- Type
#check Nat → Bool        -- Type
#check Nat → Nat         -- ...
#check Nat → Nat → Nat
#check Nat → (Nat → Nat)
#check Nat → Nat → Bool
#check (Nat → Nat) → Nat

These are all Type, which is the type of "ordinary" types. Types are themselves first-class. We can define constants for them:

def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List

#check α        -- Type
#check F α      -- Type
#check F Nat    -- Type

We said that everything has a type. So what is the type of Type?

#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5

This is a subtle part of Lean, and mostly something we can ignore: there is an infinite hierarchy of types; Type is a synonym for Type 0, and is the type of "ordinary" (or "small") types. There is one other member of this hierarchy that we need to consider: Prop, which is the type of logical statements, and is actually the lowest on the hierarchy: Prop : Type. It also has special rules, which are important for expressing theorems, but this too is something we can usually ignore.

The point of mentioning this at all is to emphasize how important it is that Lean is typed, and that the types allow us to express much richer programs than in typical languages: we can easily write functions that take types as inputs, for example, as types are themselves data (that have types one higher level on the hierarchy).