Church Numeral Puzzles

Stream: maths

[Kevin Buzzard]

I am trying to understand church numerals by writing a collection of basic theorems about them.

[Kevin Buzzard]

I just solved this one:

[Kevin Buzzard]

def chℕ := Π X : Type, (X → X) → X → X

namespace chnat

open nat

definition to_nat : chℕ → ℕ := λ m, m ℕ nat.succ 0

def of_nat : ℕ → chℕ
| (zero) := λ X f x, x
| (succ n) := λ X f x, f (of_nat n X f x) -- f (f^n x)

definition of_nat' : ℕ → chℕ
| 0 := λ X f x, x
| (n + 1) := λ X f x, of_nat' n X f (f x) -- f^n (f x)

theorem of_nat_is_of_nat' (n : ℕ) : of_nat n = of_nat' n := sorry

end chnat

[Kevin Buzzard]

it was harder than I expected though, so I probably missed a trick, which is why I mention it here.

[Gabriel Ebner]

Hmm, this was a pretty straightforward induction:

theorem of_nat_is_of_nat' (n : ℕ) : of_nat n = of_nat' n :=
begin
induction n with n; funext X f x; simp! *,
clear n_ih, induction n generalizing x; simp! *,
end

[Kevin Buzzard]

This is the key lemma I've been after:

[Kevin Buzzard]

lemma of_nat_functorial (n : ℕ) (X Y : Type) (a : X → Y) (f : X → X) : ∀ x,
a (of_nat n X f x) = @of_nat n (X → Y) (λ g x', g (f x')) a x :=

[Kevin Buzzard]

I have never used generalizing or simp! before.

[Kevin Buzzard]

So thanks very much for these!

[Kevin Buzzard]

@Gabriel Ebner

[Kevin Buzzard]

I also have this:

[Kevin Buzzard]

example (m n : ℕ) : of_nat (m + n) = of_nat m + of_nat n := sorry

[Chris Hughes]

lemma of_nat_functorial : ∀ (n : ℕ) (X Y : Type) (a : X → Y) (f : X → X) (x : X),
a (of_nat n X f x) = @of_nat n (X → Y) (λ g x', g (f x')) a x
| 0 := by intros; refl
| (n+1) := begin
  assume X Y a f x,
  rw [of_nat],
  dsimp,
  rw ← of_nat_functorial,
  dsimp,
   apply congr_arg,
   clear of_nat_functorial,
   induction n with n ih generalizing x,
   refl,
   rw of_nat,
   dsimp,
   rw ih,
end

[Chris Hughes]

Not the cleanest, but done.

[Gabriel Ebner]

These lemmas are all induction+simp, if you set them up correctly:

instance: has_add chℕ := ⟨λ a b X f, a _ f ∘ b _ f⟩
@[simp] lemma chℕ_add (a b : chℕ) : a + b = (λ X f, a _ f ∘ b _ f) := rfl

@[simp] lemma of_nat_f (n X f x) : of_nat n X f (f x) = f (of_nat n X f x) :=
by induction n generalizing x; simp! *

local attribute [-simp] add_comm
lemma of_nat_add  (m n : ℕ) : of_nat (m + n) = of_nat m + of_nat n :=
by induction n with n generalizing m; funext X f x; simp [of_nat, *]

[Gabriel Ebner]

Unfortunately you can't orient of_nat_f the other way around because it won't work as a simp lemma then.

[Kevin Buzzard]

Thanks so much Gabriel!

[Kevin Buzzard]

These proofs are really cool :-)

[Kevin Buzzard]

I understand better the way you think about the question now. I want to prove all the intermediate lemmas first, because historically I have been trained to go forwards. You just keep reducing the problem to simpler statements by induction because dependent type theory is somehow better at pushing backwards.

[Kevin Buzzard]

The one with clear n_ih is interesting!

[Kevin Buzzard]

def pow : chℕ → chℕ → chℕ :=
λ m n, λ X f x,
  n (X → X) (λ g, (m X g)) f x
theorem of_nat_pow (m n : ℕ) : of_nat (m + n) = of_nat m + of_nat n := sorry

[Mario Carneiro]

I think the proof is of_nat_add _ _ :)

[Kevin Buzzard]

wait a second

[Kevin Buzzard]

def chℕ := Π X : Type, (X → X) → X → X

namespace chnat

open nat

definition to_nat : chℕ → ℕ := λ m, m ℕ nat.succ 0

def of_nat : ℕ → chℕ
| (zero) := λ X f x, x
| (succ n) := λ X f x, f (of_nat n X f x) -- f (f^n x)

def pow : chℕ → chℕ → chℕ :=
λ m n, λ X f x,
  n (X → X) (λ g, (m X g)) f x
theorem of_nat_pow (m n : ℕ) : of_nat (m ^ n) = pow (of_nat m) (of_nat n) := sorry


end chnat

[Kevin Buzzard]

I think that runs and asks the question I want to ask :-)

[Kenny Lau]

I thought I already proved it

[Kevin Buzzard]

Can you golf it though?

[Kenny Lau]

...

[Kevin Buzzard]

Did you see Gabriel's proofs?

[Mario Carneiro]

def chℕ := Π X : Type, (X → X) → X → X

namespace chnat

open nat

def to_nat (m : chℕ) : ℕ := m ℕ nat.succ 0

def of_nat : ℕ → chℕ
| (zero) X f x := x
| (succ n) X f x := f (of_nat n X f x) -- f (f^n x)

def pow (m n : chℕ) : chℕ
| X f x := n (X → X) (m X) f x

theorem of_nat_pow (m n : ℕ) : of_nat (m ^ n) = pow (of_nat m) (of_nat n) :=
sorry

end chnat

golfed

[Kenny Lau]

...

[Kevin Buzzard]

Mario I guess that in reality I am more interested in the style. Is yours both preferable and golfier? Ultimately I want to write good style Lean.

[Kenny Lau]

I wouldn't prefer it

[Kevin Buzzard]

ooh the lam g on my part was a rookie error

[Kenny Lau]

you see, it uses the equation compiler

[Kenny Lau]

and uses "external" definitional equality

[Kenny Lau]

like it isn't "expressionally equal" but somehow they made it definitionally equal (by all those ._equation_1) thing

[Kenny Lau]

do #print prefix chnat.pow to see what I mean

[Mario Carneiro]

huh? There is no fancy business in any of the definitions except of_nat, but that was already defined by eqn compiler

[Kenny Lau]

hmm...

[Kenny Lau]

they don't do ._main if you don't have two cases?

[Mario Carneiro]

the eqn compiler always produces ._main I guess

[Mario Carneiro]

for uniformity I assume

[Kenny Lau]

I don't like main

[Kenny Lau]

as a sidenote now I prefer trans_rel_left over calc lol

[Kenny Lau]

because _ with the tactics

[Kevin Buzzard]

Oh you're right Kenny. So Mario does this mean that the lambda style is preferred in practice?

[Kenny Lau]

I think Mario prefers the equation compiler because it looks nicer

[Mario Carneiro]

I always locally optimize def T : A -> B := \lam x, t => def T (x : A) : B := t

[Mario Carneiro]

and def T : B := \lam x, t => def T : B | x := t

[Kenny Lau]

what next, \la x, A $ B x => A \o B?

[Kenny Lau]

does your optimization have church rosser?

[Mario Carneiro]

that one depends on whether the \o gets in the way later

[Mario Carneiro]

but usually yes

[Kenny Lau]

even if x is a proposition?

[Mario Carneiro]

sure, why not?

[Kenny Lau]

wow

[Kevin Buzzard]

It's the | that causes the trouble

[Mario Carneiro]

it often doesn't work as a straight replacement since it could be dependent

[Kevin Buzzard]

suddenly I have pow._main

[Kenny Lau]

yay we're on the same side for this time

[Mario Carneiro]

Yes, the | triggers the equation compiler

[Mario Carneiro]

It also gives you the correct (applied) equation lemma

[Mario Carneiro]

rather than the lambda equation lemma

[Kenny Lau]

I don't like that

[Kevin Buzzard]

But Kenny is that just because you haven't learned how to use the more complex type properly?

[Kevin Buzzard]

What is an example of where this causes you problems?

[Kenny Lau]

heh... I use the equation compiler all the time

[Kenny Lau]

I just don't like it

[Kevin Buzzard]

and I am asking why exactly

[Kenny Lau]

i don't know

[Mario Carneiro]

I understand wanting a simple underlying term, but that's an issue best aimed at the equation compiler

[Kevin Buzzard]

I am just learning all these tricks now. I have learned that when you write a substantial amount of code you end up picking stuff up as you need it; Kenny you wrote a lot of code a lot quicker than me.

[Kevin Buzzard]

Mario, did you do my Ackermann church question? ;-)

[Kenny Lau]

I'm convinced you can't do it

[Kenny Lau]

you need a higher order functional

[Kenny Lau]

since chNat lives in Type 1

[Kenny Lau]

you need an empowered chNat that lives in Type 2

[Kenny Lau]

Ackermann isn't primitive recursive

[Kenny Lau]

its image is in Delta_1 not Delta_0

[Kenny Lau]

in the arithmetic hierarchy

[Kevin Buzzard]

def ack : chℕ → chℕ → chℕ := sorry -- KB didn't try this one

[Kenny Lau]

whatever that means

[Kevin Buzzard]

(for good reason!)

[Mario Carneiro]

what ackermann church question

[Kevin Buzzard]

fill in the def above

[Kenny Lau]

@Mario Carneiro make ackermann using church

[Kevin Buzzard]

so that it commutes with usual ack on nat

[Kenny Lau]

@Kevin Buzzard or do you already know that one can't do it

[Kevin Buzzard]

I don't have a clue

[Mario Carneiro]

You can do it

[Kevin Buzzard]

I just think this is really cool :-)

[Kevin Buzzard]

How do you know you can do it?

[Kenny Lau]

@Mario Carneiro I tried to do it and found myself requiring a more complex term in each iteration

[Kenny Lau]

you can't iterate on (chN -> chN) either

[Kevin Buzzard]

When a computer scientist says "you can do it" do they mean "there exists some computer code which does that job" or "it's possible to construct, in polynomial time, some computer code which does that job"

[Kenny Lau]

the former

[Mario Carneiro]

I mean there is a solution in less than 50 chars

[Kevin Buzzard]

:-)

[Kenny Lau]

??????

[Kenny Lau]

50 chars....

[Mario Carneiro]

so just go through all the lambda terms, you'll get it

[Kevin Buzzard]

that's not polynomial time though

[Mario Carneiro]

heck no

[Kevin Buzzard]

Just to be clear, we're talking about the church numeral type without the axiom.

[Kevin Buzzard]

def chℕ := Π X : Type, (X → X) → X → X

[Kenny Lau]

@Mario Carneiro so what is wrong with my analysis?

[Mario Carneiro]

Ah, I see what you mean now

[Mario Carneiro]

In lambda calculus it's untyped so there is no problems

[Kenny Lau]

exactly

[Mario Carneiro]

but lean has universe issues

[Kenny Lau]

we're in typed lamdba calculus

[Kevin Buzzard]

as opposed to his rather more well-behaved friend chℕfree := {m : Π X : Type, (X → X) → X → X // ∀ (X Y : Type) (a : X → Y) (f : X → X) (x : X), m (X → Y) (λ g, g ∘ f) a x = a (m X f x)}

[Kevin Buzzard]

which comes with a free theorem

[Mario Carneiro]

you can still do it but you need inductive types, I think

[Kevin Buzzard]

oh wait I can do it by cheating!

[Kevin Buzzard]

There's a projection from church nat to nat

[Mario Carneiro]

exactly

[Mario Carneiro]

so you do an induction on nat -> nat

[Kenny Lau]

that's cheating

[Kevin Buzzard]

so I can define an "incorrect" pow

[Kevin Buzzard]

But this is cheating

[Kevin Buzzard]

Is this what they do with pred?

[Mario Carneiro]

like I said, you need inductive types

[Kenny Lau]

that's like asking can I define pow by of_nat and to_nat

[Kevin Buzzard]

If you were to project to nat and then project back with any of add, mul or pow

[Mario Carneiro]

I think you are right that chN only allows primrec definitions directly

[Kevin Buzzard]

you would get a different answer to the "pure" answers which exist

[Kenny Lau]

I mean there is a solution in less than 50 chars

this wouldn't work. how are you going to check if a given lambda term produces ack?

[Mario Carneiro]

solve the halting problem of course

[Kevin Buzzard]

in the proof I'm envisaging

[Kenny Lau]

you...

[Kevin Buzzard]

:-)

[Kevin Buzzard]

it's going to follow from some cunning unravelling isn't it?

[Mario Carneiro]

wait, no I lied again, it is possible

[Kenny Lau]

hmm

[Mario Carneiro]

the motive is X → X

[Kenny Lau]

you need to store a function each time

[Kevin Buzzard]

theorem nat_of_chnat_of_nat (n : ℕ) : to_nat (of_nat n) = n := sorry -- exercise

-- breakthough! I implemented my exciting new foo function on church numerals
def foo : ℕ → ℕ → ℕ := sorry
def choo (m n : chℕ) : chℕ := of_nat (foo (to_nat m) (to_nat n))

theorem amazing_compatibility (a b : ℕ) :
of_nat (foo a b) = choo (of_nat a) (of_nat b) :=
begin
unfold choo,
simp [nat_of_chnat_of_nat]
end

[Kevin Buzzard]

That makes me slightly sad

[Kevin Buzzard]

I spent some time today thinking about the Church Numeral which given X and f and x, returns x unless X = nat and f = succ and x = 0, in which case it returns 1

[Kevin Buzzard]

it's quite a good way of reminding yourself exactly how far you can expect to push things

[Kevin Buzzard]

e.g. I believe that funny numeral doesn't commute with + 1 and this can be easily checked via very concrete calculation on nat

[Kevin Buzzard]

so you know you shouldn't be trying to prove that add commutes

[Kevin Buzzard]

I'm not sure what Mr Ackermann would have thought about evaluating his function there

[Mario Carneiro]

By the way, you got the free statement a bit off:

def chℕfree := {m : Π X : Type, (X → X) → X → X //
  ∀ (X Y : Type) (a : X → Y) (f : X → X) (g : Y → Y),
  a ∘ f = g ∘ a → m Y g ∘ a = a ∘ m X f}

[Kevin Buzzard]

Do you think that's the same?

[Kevin Buzzard]

You are quantifying over g too

[Kevin Buzzard]

It might be the same

[Mario Carneiro]

It might be the same, but my version fits a more regular pattern

[Mario Carneiro]

and it doesn't require evaluating m at a function type

[Mario Carneiro]

It's basically saying that if a : f -> g is a natural transformation, then so is m

[Mario Carneiro]

That's probably a poor reading, but something like that

[Mario Carneiro]

What makes chN not quite as powerful as system T is that chN isn't a type in the internal sense

[Mario Carneiro]

with impredicative quantification (like in system F) this would work

[Mario Carneiro]

Godel's system T is simply typed lambda calculus with arrows and products, and a type N with 0 : N and S : N -> N and iter_A : (A -> A) -> A -> N -> A

[Mario Carneiro]

Then N there is just like lean's ℕ, but chℕ is not a substitute because it lives in Type 1 so it is not a type in STLC

[Kevin Buzzard]

This is really interesting

[Kevin Buzzard]

I identified nat as the universal object

[Kevin Buzzard]

and just wrote down some kind of standard maths functory thing about evaluating the universal object at a map

[Kevin Buzzard]

but, like induction, you might think about universal objects in a different way to us

[Kevin Buzzard]

I think I see what I'm missing

[Kevin Buzzard]

In my world, a would be a map in the category

[Kevin Buzzard]

and I would be assuming m was a functor

[Kevin Buzzard]

and trying to represent it

[Kevin Buzzard]

but m being a functor is an extra condition which I have forgotten about because in the examples I know it is always there

[Kevin Buzzard]

example : equiv ℕ chℕfree := ⟨to_chfr,of_chfr,inv₁,inv₂⟩

[Kevin Buzzard]

Mario's definition definitely works. I wonder if mine (which is implied by Mario's) is too weak.

[Kevin Buzzard]

So I understand the category theory language much better than this DTT stuff.

[Kevin Buzzard]

I want to say that Type is a category.

[Mario Carneiro]

It is

[Kevin Buzzard]

Then m wants to be a functor from Type to Type

[Kevin Buzzard]

but Church's naive definition just demands a map on objects

[Mario Carneiro]

In languages where the naive definition works, that's because of parametric polymorphism

[Mario Carneiro]

i.e. everything is functorial

[Kevin Buzzard]

I don't know what that means

[Mario Carneiro]

HoTT is a lot like this

[Kevin Buzzard]

Oh I see

[Mario Carneiro]

the language is crafted such that you can't write badly behaved terms at all

[Mario Carneiro]

everything is "fibrant"

[Mario Carneiro]

whatever that means

[Kevin Buzzard]

Let me modify Type

[Kevin Buzzard]

so that its objects are still terms whose type is Type

[Mario Carneiro]

but that's basically why univalence works

[Kevin Buzzard]

but the morphisms are equivs

[Kevin Buzzard]

Now m is a map on objects

[Kevin Buzzard]

and the data of the equiv is exactly what m needs to be extendible to a map on morphisms I suspect

[Mario Carneiro]

Check this out: http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf

[Kevin Buzzard]

In fact I guess it's exactly when X and Y biject that I would even dream of identifying (X->X) -> X -> X and the analogous term for Y

[Mario Carneiro]

It argues that naturality is the wrong idea and should be replaced by parametricity

[Mario Carneiro]

I need to finish digesting it though, so don't quote me on that

[Mario Carneiro]

Notice though that the condition I gave does not require that a is an equiv

[Mario Carneiro]

I think that's going to be true in general

[Mario Carneiro]

It really is a functoriality condition

[Kevin Buzzard]

You have to be careful

[Kevin Buzzard]

Given a map A to B

[Mario Carneiro]

it's just this weird higher order functoriality thing

[Mario Carneiro]

It seems like logical relations generate the condition well

[Kevin Buzzard]

You don't get a map (A to A) to (B to B)

[Kevin Buzzard]

So I don't know what you mean when you say functoriality is true "in general"

[Kevin Buzzard]

I can only see a functor in the equiv category

[Kevin Buzzard]

Maybe we mean different things by functorially

[Mario Carneiro]

I mean that if you write down some more complicated thing than chN I can write down a more complicated parametricity constraint for it

[Mario Carneiro]

and I can always do this

[Mario Carneiro]

and it will involve a function a : X -> Y

[Mario Carneiro]

and that function will usually not be required to be an equiv

[Kevin Buzzard]

I can't make that concept into a functor

[Kevin Buzzard]

For me, F (X -> Y) is a map F X -> F Y

[Mario Carneiro]

Here's the setup: we define a collection of logical relations [R] : X -> Y -> Prop. The important one is for arrows: [R -> S] : (X -> X') -> (Y -> Y') -> Prop is defined by

f [R -> S] g <-> \forall x y, x [R] y -> f x [S] g y

[Mario Carneiro]

At the base types we define [R] : X -> Y -> Prop by x [R] y <-> a x = y

[Mario Carneiro]

where a : X -> Y is our fixed morphism to commute over

[Mario Carneiro]

Applying this definition to [(R -> R) -> R -> R] gives exactly the condition I wrote down

[Kevin Buzzard]

Oh so you're going to tell me that the function I'm looking for is actually a relation

[Mario Carneiro]

And we can go further to even get the a part: we can define [∀ X, R] : (∀ X:Type, P X) -> (∀ X:Type, Q X) -> Prop by

F [∀ X, R] G <-> ∀ X Y : Type, ∀ (a : X -> Y), F X [R] G Y

(here if X appears in R it's referring to the relation for the function a)

[Mario Carneiro]

Finally, a term is parametrically polymorphic if it is related to itself at its type, i.e. m [∀ X, (X -> X) -> X -> X] m for the case of chN

[Mario Carneiro]

This is how logical relations work, and how the theorems for free statements are derived

[Kevin Buzzard]

Check this out: http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf

That paper