Stream: maths

Topic: Church Numeral Puzzles

Kevin Buzzard (May 02 2018 at 19:55):

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

Kevin Buzzard (May 02 2018 at 19:55):

I just solved this one:

Kevin Buzzard (May 02 2018 at 19:56):

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 (May 02 2018 at 19:57):

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

Gabriel Ebner (May 02 2018 at 20:06):

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 (May 02 2018 at 20:33):

This is the key lemma I've been after:

Kevin Buzzard (May 02 2018 at 20:33):

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 (May 02 2018 at 20:35):

I have never used generalizing or simp! before.

Kevin Buzzard (May 02 2018 at 20:35):

So thanks very much for these!

@Gabriel Ebner

Kevin Buzzard (May 02 2018 at 20:36):

I also have this:

Kevin Buzzard (May 02 2018 at 20:36):

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

Chris Hughes (May 02 2018 at 20:47):

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 (May 02 2018 at 20:47):

Not the cleanest, but done.

Gabriel Ebner (May 02 2018 at 20:58):

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! *

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 (May 02 2018 at 21:00):

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

Kevin Buzzard (May 02 2018 at 21:34):

Thanks so much Gabriel!

Kevin Buzzard (May 02 2018 at 22:12):

These proofs are really cool :-)

Kevin Buzzard (May 02 2018 at 22:13):

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 (May 02 2018 at 22:16):

The one with clear n_ih is interesting!

Kevin Buzzard (May 02 2018 at 22:26):

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 (May 02 2018 at 22:28):

I think the proof is of_nat_add _ _ :)

wait a second

Kevin Buzzard (May 02 2018 at 22:29):

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 (May 02 2018 at 22:29):

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

Kenny Lau (May 02 2018 at 22:29):

I thought I already proved it

Kevin Buzzard (May 02 2018 at 22:29):

Can you golf it though?

...

Kevin Buzzard (May 02 2018 at 22:29):

Did you see Gabriel's proofs?

Mario Carneiro (May 02 2018 at 22:31):

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

...

Kevin Buzzard (May 02 2018 at 22:35):

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 (May 02 2018 at 22:37):

I wouldn't prefer it

Kevin Buzzard (May 02 2018 at 22:37):

ooh the lam g on my part was a rookie error

Kenny Lau (May 02 2018 at 22:37):

you see, it uses the equation compiler

Kenny Lau (May 02 2018 at 22:37):

and uses "external" definitional equality

Kenny Lau (May 02 2018 at 22:38):

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

Kenny Lau (May 02 2018 at 22:38):

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

Mario Carneiro (May 02 2018 at 22:39):

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

hmm...

Kenny Lau (May 02 2018 at 22:40):

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

Mario Carneiro (May 02 2018 at 22:40):

the eqn compiler always produces ._main I guess

Mario Carneiro (May 02 2018 at 22:40):

for uniformity I assume

Kenny Lau (May 02 2018 at 22:43):

I don't like main

Kenny Lau (May 02 2018 at 22:44):

as a sidenote now I prefer trans_rel_left over calc lol

Kenny Lau (May 02 2018 at 22:44):

because _ with the tactics

Kevin Buzzard (May 02 2018 at 22:45):

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

Kenny Lau (May 02 2018 at 22:46):

I think Mario prefers the equation compiler because it looks nicer

Mario Carneiro (May 02 2018 at 22:46):

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

Mario Carneiro (May 02 2018 at 22:47):

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

Kenny Lau (May 02 2018 at 22:47):

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

Kenny Lau (May 02 2018 at 22:48):

does your optimization have church rosser?

Mario Carneiro (May 02 2018 at 22:48):

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

but usually yes

Kenny Lau (May 02 2018 at 22:48):

even if x is a proposition?

sure, why not?

wow

Kevin Buzzard (May 02 2018 at 22:49):

It's the | that causes the trouble

Mario Carneiro (May 02 2018 at 22:49):

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

Kevin Buzzard (May 02 2018 at 22:49):

suddenly I have pow._main

Kenny Lau (May 02 2018 at 22:49):

yay we're on the same side for this time

Mario Carneiro (May 02 2018 at 22:49):

Yes, the | triggers the equation compiler

Mario Carneiro (May 02 2018 at 22:50):

It also gives you the correct (applied) equation lemma

Mario Carneiro (May 02 2018 at 22:50):

rather than the lambda equation lemma

Kenny Lau (May 02 2018 at 22:50):

I don't like that

Kevin Buzzard (May 02 2018 at 22:51):

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

Kevin Buzzard (May 02 2018 at 22:51):

What is an example of where this causes you problems?

Kenny Lau (May 02 2018 at 22:51):

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

Kenny Lau (May 02 2018 at 22:51):

I just don't like it

Kevin Buzzard (May 02 2018 at 22:51):

and I am asking why exactly

i don't know

Mario Carneiro (May 02 2018 at 22:52):

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

Kevin Buzzard (May 02 2018 at 22:53):

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 (May 02 2018 at 22:53):

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

Kenny Lau (May 02 2018 at 22:53):

I'm convinced you can't do it

Kenny Lau (May 02 2018 at 22:53):

you need a higher order functional

Kenny Lau (May 02 2018 at 22:54):

since chNat lives in Type 1

Kenny Lau (May 02 2018 at 22:54):

you need an empowered chNat that lives in Type 2

Kenny Lau (May 02 2018 at 22:54):

Ackermann isn't primitive recursive

Kenny Lau (May 02 2018 at 22:54):

its image is in Delta_1 not Delta_0

Kenny Lau (May 02 2018 at 22:54):

in the arithmetic hierarchy

Kevin Buzzard (May 02 2018 at 22:54):

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

Kenny Lau (May 02 2018 at 22:54):

whatever that means

Kevin Buzzard (May 02 2018 at 22:54):

(for good reason!)

Mario Carneiro (May 02 2018 at 22:54):

what ackermann church question

Kevin Buzzard (May 02 2018 at 22:54):

fill in the def above

Kenny Lau (May 02 2018 at 22:54):

@Mario Carneiro make ackermann using church

Kevin Buzzard (May 02 2018 at 22:55):

so that it commutes with usual ack on nat

Kenny Lau (May 02 2018 at 22:55):

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

Kevin Buzzard (May 02 2018 at 22:55):

I don't have a clue

You can do it

Kevin Buzzard (May 02 2018 at 22:55):

I just think this is really cool :-)

Kevin Buzzard (May 02 2018 at 22:55):

How do you know you can do it?

Kenny Lau (May 02 2018 at 22:56):

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

Kenny Lau (May 02 2018 at 22:56):

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

Kevin Buzzard (May 02 2018 at 22:57):

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"

the former

Mario Carneiro (May 02 2018 at 22:57):

I mean there is a solution in less than 50 chars

:-)

??????

50 chars....

Mario Carneiro (May 02 2018 at 22:57):

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

Kevin Buzzard (May 02 2018 at 22:57):

that's not polynomial time though

heck no

Kevin Buzzard (May 02 2018 at 22:58):

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

Kevin Buzzard (May 02 2018 at 22:59):

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

Kenny Lau (May 02 2018 at 22:59):

@Mario Carneiro so what is wrong with my analysis?

Mario Carneiro (May 02 2018 at 22:59):

Ah, I see what you mean now

Mario Carneiro (May 02 2018 at 23:00):

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

exactly

Mario Carneiro (May 02 2018 at 23:00):

but lean has universe issues

Kenny Lau (May 02 2018 at 23:00):

we're in typed lamdba calculus

Kevin Buzzard (May 02 2018 at 23:00):

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 (May 02 2018 at 23:00):

which comes with a free theorem

Mario Carneiro (May 02 2018 at 23:00):

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

Kevin Buzzard (May 02 2018 at 23:01):

oh wait I can do it by cheating!

Kevin Buzzard (May 02 2018 at 23:01):

There's a projection from church nat to nat

exactly

Mario Carneiro (May 02 2018 at 23:01):

so you do an induction on nat -> nat

that's cheating

Kevin Buzzard (May 02 2018 at 23:02):

so I can define an "incorrect" pow

Kevin Buzzard (May 02 2018 at 23:02):

But this is cheating

Kevin Buzzard (May 02 2018 at 23:02):

Is this what they do with pred?

Mario Carneiro (May 02 2018 at 23:02):

like I said, you need inductive types

Kenny Lau (May 02 2018 at 23:02):

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

Kevin Buzzard (May 02 2018 at 23:02):

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

Mario Carneiro (May 02 2018 at 23:02):

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

Kevin Buzzard (May 02 2018 at 23:02):

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

Kenny Lau (May 02 2018 at 23:03):

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 (May 02 2018 at 23:04):

solve the halting problem of course

Kevin Buzzard (May 02 2018 at 23:04):

in the proof I'm envisaging

you...

:-)

Kevin Buzzard (May 02 2018 at 23:04):

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

Mario Carneiro (May 02 2018 at 23:09):

wait, no I lied again, it is possible

hmm

Mario Carneiro (May 02 2018 at 23:09):

the motive is X → X

Kenny Lau (May 02 2018 at 23:10):

you need to store a function each time

Kevin Buzzard (May 02 2018 at 23:18):

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 (May 02 2018 at 23:21):

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 (May 02 2018 at 23:22):

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

Kevin Buzzard (May 02 2018 at 23:24):

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 (May 02 2018 at 23:24):

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

Kevin Buzzard (May 02 2018 at 23:25):

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

Mario Carneiro (May 02 2018 at 23:26):

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 (May 02 2018 at 23:30):

Do you think that's the same?

Kevin Buzzard (May 02 2018 at 23:30):

You are quantifying over g too

Kevin Buzzard (May 02 2018 at 23:31):

It might be the same

Mario Carneiro (May 02 2018 at 23:34):

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

Mario Carneiro (May 02 2018 at 23:34):

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

Mario Carneiro (May 02 2018 at 23:35):

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

Mario Carneiro (May 02 2018 at 23:36):

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

Mario Carneiro (May 02 2018 at 23:38):

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

Mario Carneiro (May 02 2018 at 23:38):

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

Mario Carneiro (May 02 2018 at 23:41):

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 (May 02 2018 at 23:42):

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 (May 02 2018 at 23:49):

This is really interesting

Kevin Buzzard (May 02 2018 at 23:49):

I identified nat as the universal object

Kevin Buzzard (May 02 2018 at 23:49):

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

Kevin Buzzard (May 02 2018 at 23:50):

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

Kevin Buzzard (May 02 2018 at 23:50):

I think I see what I'm missing

Kevin Buzzard (May 02 2018 at 23:51):

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

Kevin Buzzard (May 02 2018 at 23:51):

and I would be assuming m was a functor

Kevin Buzzard (May 02 2018 at 23:51):

and trying to represent it

Kevin Buzzard (May 02 2018 at 23:51):

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 (May 03 2018 at 01:12):

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

Kevin Buzzard (May 03 2018 at 01:17):

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

Kevin Buzzard (May 03 2018 at 01:23):

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

Kevin Buzzard (May 03 2018 at 01:23):

I want to say that Type is a category.

It is

Kevin Buzzard (May 03 2018 at 01:23):

Then m wants to be a functor from Type to Type

Kevin Buzzard (May 03 2018 at 01:23):

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

Mario Carneiro (May 03 2018 at 01:24):

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

Mario Carneiro (May 03 2018 at 01:24):

i.e. everything is functorial

Kevin Buzzard (May 03 2018 at 01:24):

I don't know what that means

Mario Carneiro (May 03 2018 at 01:24):

HoTT is a lot like this

Oh I see

Mario Carneiro (May 03 2018 at 01:24):

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

Mario Carneiro (May 03 2018 at 01:25):

everything is "fibrant"

Mario Carneiro (May 03 2018 at 01:25):

whatever that means

Kevin Buzzard (May 03 2018 at 01:25):

Let me modify Type

Kevin Buzzard (May 03 2018 at 01:25):

so that its objects are still terms whose type is Type

Mario Carneiro (May 03 2018 at 01:25):

but that's basically why univalence works

Kevin Buzzard (May 03 2018 at 01:25):

but the morphisms are equivs

Kevin Buzzard (May 03 2018 at 01:25):

Now m is a map on objects

Kevin Buzzard (May 03 2018 at 01:26):

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

Kevin Buzzard (May 03 2018 at 01:27):

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 (May 03 2018 at 01:27):

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

Mario Carneiro (May 03 2018 at 01:27):

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

Mario Carneiro (May 03 2018 at 01:28):

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

Mario Carneiro (May 03 2018 at 01:28):

I think that's going to be true in general

Mario Carneiro (May 03 2018 at 01:28):

It really is a functoriality condition

Kevin Buzzard (May 03 2018 at 01:29):

You have to be careful

Kevin Buzzard (May 03 2018 at 01:29):

Given a map A to B

Mario Carneiro (May 03 2018 at 01:29):

it's just this weird higher order functoriality thing

Mario Carneiro (May 03 2018 at 01:29):

It seems like logical relations generate the condition well

Kevin Buzzard (May 03 2018 at 01:29):

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

Kevin Buzzard (May 03 2018 at 01:30):

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

Kevin Buzzard (May 03 2018 at 01:30):

I can only see a functor in the equiv category

Kevin Buzzard (May 03 2018 at 01:31):

Maybe we mean different things by functorially

Mario Carneiro (May 03 2018 at 01:31):

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 (May 03 2018 at 01:31):

and I can always do this

Mario Carneiro (May 03 2018 at 01:31):

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

Mario Carneiro (May 03 2018 at 01:32):

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

Kevin Buzzard (May 03 2018 at 01:33):

I can't make that concept into a functor

Kevin Buzzard (May 03 2018 at 01:34):

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

Mario Carneiro (May 03 2018 at 01:35):

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 (May 03 2018 at 01:36):

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

Mario Carneiro (May 03 2018 at 01:36):

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

Mario Carneiro (May 03 2018 at 01:37):

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

Kevin Buzzard (May 03 2018 at 01:37):

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

Mario Carneiro (May 03 2018 at 01:42):

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 (May 03 2018 at 01:43):

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 (May 03 2018 at 01:44):

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

Kevin Buzzard (May 03 2018 at 15:34):

That paper

Last updated: May 18 2021 at 08:14 UTC