Last time we established the concept of an inductive structure. Before we get to what unique readability, we’ll have to talk a little more about inductive structures.
We will use to refer to the domain of in these notes.
Also, from now on, when we say “the closure of ”, we mean the minimal set such that is closed under .
Before, we were dealing with functions that possibly had tuples of different sizes in its domain. For instance, maybe can take arguments sometimes, and arguments at other times. For the purposes of an inductive structure, we can decompose such a function into and , the subsets of the functions that take and functions respectively. This would not alter the closure whatsoever, so for the remainder of these notes we will make that simplification.
If a function takes inputs, then we say it is -ary. Alternatively, we say that is its arity. Both terms are synonymous.
Theorem. Let be some property and be an inductive structure. If is a property such that
- all satisfy
- for all and all tuples , if all satisfy then does too.
then all elements in the closure of satisfy as well.
This is what a proof by induction looks like. First we prove the base case: all satisfy . Then we prove the inductive step: applying a function to a tuple of stuff that satisfies spits out something that also satisfies .
Consider the inductive structure that generates the natural numbers. Whenever we do a standard proof by induction, this is the closure we are implicitly using. But hopefully you see just how powerful this theorem is.
Outline of proof. Recall how we constructed sets to show that has a closure. Now we can inductively prove that every satisfies .
Motivating example: propositional logic
These notes will assume a little bit of CS knowledge and no knowledge of propositional logic. If you know the latter, you can probably skim or even entirely skip this section.
So perhaps you are familiar with boolean operators such as
(a && (!b)) || c
Propositional logic works a similar way: we have formulae composed of
propositional letters — like
are in the example above, though they can be anything — and operators
act on some number of propositional letters. However, in classical logic
(the form of propositional logic we usually study) we use different
symbols to represent the AND, OR, and NOT operators: they are
Well, the formulae in a propositional logic can also be represented as a closure of an inductive structure! For example, consider an inductive structure such that . Note that there is an function that returns a string with an symbol, and the two are not the same. Furthermore, note that the and characters are part of the outputted string. We can similarly define .
Here’s why we need the parentheses: ignore for a second what you know about operator precedence. Consider a formula like . Should it represent , or should it represent ? Another way to think of it is, without the parentheses, how was this propositional formula inductively generated: as , or as ? Thus it is useful for formulae to be generated in one unique way. It is useful for propositional formulae to be uniquely readable (which they are, solely because of the parentheses).
Definition (Unique Readability). An inductive structure is uniquely readable if and only if for every in its closure , exactly one of the following conditions hold:
- there is exactly one and exactly one tuple . such that and for .
Note that the inductive structure is uniquely readable. Try proving this yourself if you don’t understand why this is true!
This notion of unique readability leads to the concept of defining a function recursively. We will first explore the properties we generally want a definition by recursion to have, then establish a theorem that formalizes all of these concepts.
First, note that a definition by recursion does not always go off without a hitch. Consider some inductive structure with , , and , . Then if and , a recursive definition based on and might run into issues — what if ? Guaranteeing this is true in general is hard, so instead we want there to be one unique set of inputs that generates this output. In other words, we want injectivity, which comes from unique readability.
Here is our wishlist for a definition by recursion. For our starting set in with closure , we want to specify:
- a subset of a function on
- specify how to compute for by taking the unique and unique tuple , and then defining using , , , , , , .
More broadly, we can define a function on a closure just by looking at the starting set and a set of compositions on elements in the starting set to define .
Of course, for the reasons we have just established, should be uniquely readable.
Now we’re ready to formalize this idea.
Theorem (Definition by recursion). Consider a uniquely readable inductive structure with closure . If
- we are given a function with
- for every , if is -ary, we are given a -ary function where ,
then there is a unique function such that
- for all , we have
- for all and all and , we have .
This specifies a unique way to extend given an inductive structure and for each .
Outline of proof: Recall the definition of when we showed the existence of a closure. We show by inducting on that there exists only one possible extension of , whose domain is , onto , whose domain is .
Here is an example of a definition by recursion on the Fibonacci sequence. Our inductive structure is where for , and its domain is only pairs of the form for .
Now we define an initial function such that and . Define , and note . Yay! Our idea of unique readability and a definition of recursion makes sense on a simple function like the Fibonacci sequence, even if it is a little convoluted.
Though it is convoluted and we will not usually need to construct recursive functions like this, it is good to know what is happening under the hood. And it is good to understand why the Fibonacci sequence gives you a well-defined, unique value of for all . It is because the Fibonacci sequence is equivalent to a function on a uniquely readable closure , as we have just shown.