Proving the beauty of a mind

In the previous Theory Lunch talk we introduced the notion of Nash equilibrium for games in normal form. Today, we went through the proof of Nash’s theorem of existence of mixed strategy Nash equilibria for finite games in normal form.

Let us recall the basic notions. In a game in normal form we have: Continue reading

Playing with a beautiful mind

Today’s talk’s topic is an idea so important in game theory, and with so many applications in different fields including computer science, that it earned its discoverer, together with Reinhard Selten and John Harsanyi, the 1994 Nobel Memorial Prize in Economic Sciences.

To introduce this idea, together with other basic game-theoretic notions, we resort to some examples. Here goes the first one: Continue reading

Many choices from few parameters

At the end of March I gave a talk about how to obtain a wide range of Bernoulli distributions with as few parameters as possible. This originates from the needs of simulations of complex systems with cellular automata machine. The solution I described comes from Mark Smith’s doctoral thesis, performed under the supervision of Tommaso Toffoli.

I wrote a post on this on my blog on cellular automata.


Transgressing the limits

Today, the 14th of January 2014, we had a special session of our Theory Lunch. I spoke about ultrafilters and how they allow to generalize the notion of limit.

Consider the space \ell^\infty of bounded sequences of real numbers, together with the supremum norm. We would like to define a notion of limit which holds for every \{x_n\}_{n \geq 0} \in \ell^\infty and satisfies the well known properties of standard limit: Continue reading

Natural numbers with addition form a monoid

The other day I gave a very short introductory talk on formalising mathematics in Agda to a highly mathematically literate but otherwise quite general audience. I presented this example.

In Agda, proofs and programs are the same thing, types are sets are propositions. These sets contain values of that type, or equally they contain proofs of that proposition.
Agda is a very expressive language so very little is built in and most things can be defined in a library. We will define some of those things now to see how they work.

module talk where

Natural numbers (0,1,2,3,…) can be seen as being defined by either zero or the successor (+1) suc of another natural number.

data Nat : Set where
  zero : Nat 
  suc  : Nat → Nat

Addition _+_ takes two natural numbers and returns another. It can be defined by recursion (induction) on the first argument. If it is zero we return n and if it is successor we can make a recursive call to (m + n) and apply the successor to the result. The recursive call (inductive hypothesis) is valid as m is structurally smaller than suc m.

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc (m + n)

Having defined one function we now want to prove something about it. One can think of this as an exercise in formal verification. I want to prove that _+_ satisfies some equations. There is an equals sign in the definition above but this is not the one I should use to state my equations. The = is the definitional equality symbol and denotes equations that the computer can see are true. I want to prove some things that the computer isn’t able to see for itself.

The notion we need is propositional equality which is a relation we will define now. In another language one might expect a relation to have type like Nat → Nat → Bool which might return true if the natural numbers were equal. In Agda we would use Set instead of Bool and the set would be inhabited if the relation holds. We can define propositional equality _≅_ once and for all for any set A which we write as an implicit parameter {A : Set}. Remarkably this set has only one canonical inhabitant refl which is inhabits the type of equations between really identical (definitionally equal) values. This may seem strange but one can prove (derive) the other properties, such as symmetry and transitivity.

-- propositional equality 
data _≅_ {A : Set} : A → A → Set where
  refl : ∀{a} → a ≅ a

We could prove useful lemmas such as symmetry now but for this post I will only need cong – that functions preserve equality. Given any function f : A → B and two equal elements of A the function should return equal results.
The lemma is very easy to prove as when we pattern match on the proof that the elements are equal then the only possible pattern is refl which forces a and a' to be equal, replacing, say, a' with a which reduces our task to showing that f a ≅ f a. This is easily proved using refl.

-- lemma: functions preserve equality
cong : {A B : Set} → (f : A → B) → {a a' : A} → a ≅ a' → f a ≅ f a'
cong f refl = refl

The lemma is very useful for proving equations that have the same function (such as suc) on both sides. We can use it to reduce our task to proving that what is underneath the function on both sides is equal.

One can define an algebraic structure like a monoid as a record (named tuple/struct/etc.) in Agda. It contains fields for the data and also for the laws. A monoid has a carrier set M a distinguished unit element e and a binary operation op. The three laws state that op has e as its left and right unit and it is associative. The monoid record Mon lives in Set1 as it contains a Set(0).

-- Monoid
record Mon : Set1 where
  -- data
  field M     : Set
        e     : M 
        op    : M → M → M
  -- laws
        lunit : ∀ m → op e m ≅ m
        runit : ∀ m → op m e ≅ m
        assoc : ∀ m n o → op (op m n) o ≅ op m (op n o)

The goal is to define a monoid where M = Nat, e = zero and op = _+_. Let’s go ahead and prove the laws. The first law which would be (zero + n) ≅ n doesn’t require proof as it holds definitionally (it is the first line of the definition of _+_). The second law does require proof as here the _+_ doesn’t compute as the first argument is the variable n.

+runit : ∀ n → (n + zero) ≅ n
+runit zero    = refl
+runit (suc n) = cong suc (+runit n)

We prove the second law +runit by induction on n. When proving a property of a program as we are doing here it’s a good idea to follow the same pattern in the proof as in the program. Here _+_ is defined by recursion on its first argument so it makes sense to carry out the proof by induction on the first argument too. This makes things compute nicely. The first case is zero + zero ≅ zero which Agda computes to zero ≅ zero by applying the definition of _+_. This is easily proved by refl. The second case computes to suc (n + zero) ≅ suc n. First we observe that there is a function suc on both sides so we type cong suc ?. This reduces our problem to proving that n + zero ≅ n which follows from the inductive hypothesis +runit n

+assoc : ∀ m n o → ((m + n) + o) ≅ (m + (n + o))
+assoc zero    n o = refl
+assoc (suc m) n o = cong suc (+assoc m n o)

The proof for associativity proceeds analogously. We pattern match on the first argument m which gives two cases. The first case computes to n + o ≅ n + o and the second computes to suc ((m + n) + o) ≅ suc (m + (n + 0)). As before the first case follows by reflexivity and the second case by congruence of suc and inductive hypothesis.

Having done all the hard work we can now define a monoid for Nat, _+_, and zero:

-- natural numbers with addition form a monoid
NatMon : Mon 
NatMon = record {
  M     = Nat; 
  e     = zero; 
  op    = _+_; 
  lunit = λ _ → refl; -- this one doesn't require proof
  runit = +runit; 
  assoc = +assoc}

Homotopy before type theory

Last Friday, the 18th of October, I talked about homotopy and the fundamental group. As I heard about homotopy type theory, I thought that reviewing what I know of the geometric part could be useful. So I prepared this talk, using Allen Hatcher’s free textbook.

Consider a continuous line on the whiteboard, from point x_0 to point x_1, and another continuous line from point y_0 to point y_1. Think of a bijection between the two lines: Continue reading