At today’s Theory Lunch I discussed limit languages of cellular automata, and Lyman Hurd’s example of a CA whose limit language is not regular. I wrote about this on my other blog.

# 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.

Link: http://anotherblogonca.wordpress.com/2014/05/15/random-settings-in-cellular-automata-machines/

# 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 of bounded sequences of real numbers, together with the supremum norm. We would like to define a notion of limit which holds for *every* 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}

# Dependently typed type checking

Today we discussed a type checker for simply typed lambda calculus written in Agda that Ulf Norell presented in his ICFP 2013 invited talk. Another version can be found in *The view from the left* by Conor McBride and James McKinna.