# Inductively Defined Lists and Proofs

In this post, we will explore an inductive data structure as a type for lists of elements. We define two recursive functions that can be applied to lists of this type; namely, an operation to append two lists and an operation to reverse a list. With these definitions, we set out to mathematically prove a number of properties that should hold for these functions by means of induction.

A list is a data structure of a collection of elements in a certain order. A list can be defined in multiple ways. One way is to define a list as being an element (the “head” of the list) followed by another list (the “tail” of the list). Inductively, this could be formalized as follows:

Inductive list a := cons a list | nil.

This means that a list l with elements of type a is either cons x tail, with x of type a and with tail of type list a, or l is the empty list nil. Let’s look at some example lists with elements of the whole numbers.

// Empty list; []
l = nil

// List with one element; [1]
l = cons 1 nil

// Different list with one element; [2]
l = cons 2 nil

// List with two elements; [1,2]
l = cons 1 (cons 2 nil)

// List with three elements; [1,2,3]
l = cons 1 (cons 2 (cons 3 nil))

Note that because we have lists of integers, following our definition the list l is of type list integer.

Multiple list operations can be defined, such as append and reverse. We defined our list inductively, and so it would make sense to define these operations inductively (also known as recursively) as well. Because of our neat data structure and operations, we should then be able to prove that certain properties of the operations hold.

# An Introduction to Turing Machines

A Turing machine is a mathematical model of a mechanical machine. At its roots, the Turing machine uses a read/write head to manipulate symbols on a tape. It was invented by the computer scientist Alan Turing in 1936. Interestingly, according to the Church-Turing thesis this simple machine can do everything any other computer can do; including our contemporary computers. Though these machines are not a practical or efficient means to calculate something in the real world, they can be used to reason about computability and other properties of computer programs.

# Alan Turing Quote from Computing Machinery and Intelligence

The view that machines cannot give rise to surprises is due, I believe, to a fallacy to which philosophers and mathematicians are particularly subject. This is the assumption that as soon as a fact is presented to a mind all consequences of that fact spring into the mind simultaneously with it. It is a very useful assumption under many circumstances, but one too easily forgets that it is false.

— Alan Turing, 1950