CPP paper

Stream: general

[Rob Lewis]

I'm submitting a paper about the p-adics and Hensel's lemma to CPP. If anyone is interested in taking a look, the paper is here: http://robertylewis.com/padics/padics.pdf I'm happy to hear any comments before or after the submission deadline on Thursday!

[Rob Lewis]

By the way, CPP (https://popl19.sigplan.org/track/CPP-2019#) is one of the main venues for publishing about formalizations. ITP (http://itp19.cecs.pdx.edu/) is another.

[Kevin Buzzard]

I am really interested in this idea and in the CS culture in general. Mathematicially you have done something which is 100 years old so the new ideas are not there. In computer science I would imagine that you are not the first person to formalise Hensel's Lemma. Am I wrong about this? And even if someone else had done it in Mizar in 2009 or whatever -- would this matter? I am trying to work out which notions of "value" a potential referee would attach to a paper such as this.

[Kevin Buzzard]

Obviously I ask because if I get the schemes repo and/or the perfectoid repo into shape then I will be thinking about the same sort of thing, but I have no idea how it works.

[Kevin Buzzard]

I see -- in section 6 you are perhaps claiming that as far as you know, Hensel's Lemma for the p-adics has not ever been done before.

[Johan Commelin]

@Rob Lewis Typo in section 6. You write "Metmath"

[Johan Commelin]

Also, congrats with the draft :wink:

[Kevin Buzzard]

If I were supervising a Masters student who wanted to do something involving Hensel's Lemma I would have told them to prove it for an arbitrary complete DVR and then prove that the p-adic numbers are a complete DVR. The fact that this machinery is not in Lean somehow makes this less convenient. Yes, let me also congratulate you on the draft :-)

[Kevin Buzzard]

The philosophy here is that proving Hensel's Lemma for the p-adics is a way of putting the library through its paces. How did you get the status of Hensel's Lemma in all the gazillion other proof assistants? Presumably I'll have to do this with schemes one day.

[Johan Commelin]

Presumably I'll have to do this with schemes one day.

I think that is a lot easier. I'm pretty sure nobody has done that before. (Although I've seen slides by Coquand on constructive algebraic geometry. But that didn't do any sheaves. It just defined Spec A as a locale [~~ open_set].)

[Rob Lewis]

The expectation for this kind of paper is that the subject hasn't been formalized before, or that you've formalized it in a novel and interesting way, and typically that it's part of some broader project. It isn't novel math, but it's a novel formalization, that shows off features of Lean and mathlib, that's a building block for work we plan to do in the future. And of course there's no guarantee that it gets accepted!

[Rob Lewis]

@Johan Commelin Thanks, fixed :slight_smile:

[Rob Lewis]

There aren't really a gazillion other proof assistants to check. It's easy enough to see what's in the Isabelle AFP, Mizar MML, and HOL Light library, they're all pretty self-contained.

[Rob Lewis]

Coq is trickier since it's a bit more fragmented, but Google "p-adic numbers coq" or "hensel's lemma coq" turns up what exists.

[Kevin Buzzard]

There aren't really a gazillion other proof assistants to check. It's easy enough to see what's in the Isabelle AFP, Mizar MML, and HOL Light library, they're all pretty self-contained.

Maybe for you -- it sounds a bit scary to me! I can't even read mathlib, and that's in a language that I kind-of know! Have schemes or perfectoid spaces been done before?

But your message answers my question very well -- thanks. I saw that someone had a paper or some sort of a write-up at least on formalising localisation of a ring in some other theorem prover and my first thought was "Kenny did that in Lean when he was a first year undergrad". If you want to explain another reason why it's part of a broader project, you can say that it's part of the 4th year undergrad curriculum at Imperial College London (p-adic numbers and Hensel's Lemma are part of the elliptic curves course, which I designed about 15 years ago) so they're an essential part of my plan to digitise the entire pure maths curriculum! And anyway, this universe is so real-number-centred and I've never understood why, the p-adic numbers are just another completion of the rationals, I don't know why we don't teach them to schoolkids.

[Rob Lewis]

Have schemes or perfectoid spaces been done before?

I strongly suspect that they haven't. A quick look at Google doesn't turn up anything relevant for perfectoid spaces. This is a new and deep concept, if it's been formalized it won't have been done silently. Schemes are harder to search for because the word is used another way in logic, but I don't see anything at a glance.

[Rob Lewis]

http://fm.mizar.org/fm.bib is a quick way to search through the Mizar library. https://www.isa-afp.org/topics.html to see significant developments in Isabelle, although not everything done in Isabelle is there.

[Rob Lewis]

https://github.com/math-comp/math-comp is maybe the most likely place to find these sorts of things in Coq, and you can use the normal GitHub search there. But there are other unconnected Coq libraries.

[Kevin Buzzard]

Thanks so much for the algorithm Rob!

[Rob Lewis]

Just remember it isn't a decision procedure!

[Tobias Grosser]

Very nice!

[Tobias Grosser]

Does it make sense to reference the git hash of mathlib/lean version u are using in the paper?

[Tobias Grosser]

Also, I spend some time reading about math yesterday to learn about p-adic numbers. So your paper comes at a very convenient point.

[Tobias Grosser]

Put it already on my reading list.

[Tobias Grosser]

I already have one question: "AFAIU 2's complement representation used to represent numbers in computers is a special case of p-adic number, right?"

[Tobias Grosser]

Does your representation require p to be prime?

[Tobias Grosser]

I wonder if existing decision procedures for Presburger arithmetic could apply directly to p-adic numbers or if instead one would need to explicitly model the "wrapping" using existentially quantified variables over a domain \mathbb{Z}.

[Kenny Lau]

nothing uncountable can be decidable

[Tobias Grosser]

OK, I need to understand this in more detail.

[Tobias Grosser]

Likely p-adic numbers in full generality may be undecidable, but the special case of 2's complement representation used on computers is certainly decidable.

[Tobias Grosser]

I am not sure what the delta is in between.

[Tobias Grosser]

http://www.numericana.com/answer/p-adic.htm

[Tobias Grosser]

Explains how two's complements in computers related to p-adic numbers.

[Kevin Buzzard]

The problem is that a 2-adic number is an infinite string of 0s and 1s

[Kevin Buzzard]

so just like the reals there's no way to decide if two 2-adic numbers are equal because you don't know whether they're going to be different at the term after you got tired checking

[Tobias Grosser]

Right. So in computers we always have finite lenght integers, such that after bit 32 all outer bits are dropped, aka assumed to have the same value than bit 32.

[Kevin Buzzard]

that would be like doing real numbers to 32 significant figures

[Tobias Grosser]

Right.

[Tobias Grosser]

That should then be trivially decidable, afaiu.

[Kevin Buzzard]

so your system sounds more like $\mathbb{Z}/2^n\mathbb{Z}$ where $n$ is the number of bits you want to spend storing your numbers

[Kevin Buzzard]

but the 2-adic integers are the limit of these things -- the projective limit, if you're a mathematician -- as $n$ goes to infinity.

[Tobias Grosser]

I see.

[Tobias Grosser]

AFAIU Z/2^n Z gives just positive numbers

[Tobias Grosser]

2's complement representation allows to reason about positive and negative numbers with one bit indicating the sign and n-1 bits indicating the value.

[Kevin Buzzard]

but that bit which indicates the sign is just disappearing off to infinity in the limit, and disappears completely by the time you got there

[Kevin Buzzard]

The CS model isn't a very good one for understanding the 2-adic integers. You could think of it as an infinite string of bits, and at some point you're hoping that you'll be told what the sign is, but actually you never get to that information.

[Tobias Grosser]

Is the reason that towards infinity the digits might switch from 0 to 1 and vice versa?

[Tobias Grosser]

So only if you know that all what is left is an infinite sequence of '0' and '1' you know the sign, right?

[Johan Commelin]

No, there is no notion of positivity for p-adics. This is one of the main "problems" in arithmetic.

[Kenny Lau]

so we can represent each 2-adic integer as a sequence (A, BA, CBA, DCBA, EDCBA, ...) where each letter is 0 or 1.
-5 would correspond to (1, 11, 011, 1011, 11011, 111011, 1111011, ...)

[Kenny Lau]

5 would correspond to (1, 01, 101, 0101, 00101, 000101, 0000101, ...)

[Kenny Lau]

and you can write them more compactly as ....1111111011 and .....000000101

[Kevin Buzzard]

The problem with saying "we can define the sign if it's all 1's from here" is that you've only defined the sign on 0% of the 2-adic numbers.

[Kevin Buzzard]

For a general 2-adic number there is no good notion of sign

[Kenny Lau]

but a dense set :P

[Tobias Grosser]

In CS, we are only interested in this finite subset of the p-adic numbers, I feel.

[Kevin Buzzard]

(i.e. not one which is continuous, or which has basic algebraic properties etc)

[Tobias Grosser]

Probably the concept is way too general for what I would like to use it for.

[Kevin Buzzard]

Modelling an abstract mathematical object like the reals by a concrete CS type such as a float means that you lose information (as far as we are concerned). In applications this might not be an issue, but in maths it is.

[Tobias Grosser]

Sure, I don't want to squeeze all 2-adic numbers in fixed-size integers.

[Tobias Grosser]

This is hopeless.

[Mario Carneiro]

The two's complement representation of an integer coincides with its 2-adic expansion as $\mathbb Z$ embedded in $\mathbb Z_2$

[Tobias Grosser]

I see.

[Tobias Grosser]

Thanks @Mario Carneiro for explaining this.

[Kevin Buzzard]

Just like you can't squeeze all real numbers into 32 bits. But here is a consequence -- it means that you have trouble distinguishing rational from irrational numbers in float because you've lost information which from a "am I far from the right answer" position is small, but from a "have I lost any arithmetic information" is big

[Tobias Grosser]

Would it make sense to e.g. define Cooper over this domain?

[Kevin Buzzard]

There's no inequalities either, if you need inequalities

[Mario Carneiro]

sure, I mean it's still the integers, but it's not easier

[Mario Carneiro]

nothing uncountable can be decidable

This is an interesting statement. I wonder how you would prove this

[Kenny Lau]

however given two explicit terms of type p_adic_integer -> nat, you can decide if they are equal. (This is a meta-theorem, not a theorem)

[Kenny Lau]

nothing uncountable can be decidable

This is an interesting statement. I wonder how you would prove this

that's a meta-theorem as well

[Mario Carneiro]

false

[Kenny Lau]

hmm?

[Mario Carneiro]

You can do the same tricks as in R to construct numbers whose equality is equivalent to the halting problem

[Kenny Lau]

right, but I mean terms that are constructed explicitly and constructively

[Mario Carneiro]

even so

[Kenny Lau]

i.e. computable functions

[Tobias Grosser]

@Kevin Buzzard, I need to read more of this but this is a paper I want to read regarding this issue: https://arxiv.org/pdf/1602.07209.pdf

[Mario Carneiro]

computable number equality is not decidable

[Mario Carneiro]

even though it is a countable set

[Mario Carneiro]

so the converse of your statement is false

[Kenny Lau]

i.e. you can't say "the n-th bit is 1 if this program terminates at the n-th step"

[Kenny Lau]

that won't be a computable function

[Mario Carneiro]

that's a computable function

[Kenny Lau]

ah wait

[Mario Carneiro]

termination in n steps is decidable

[Kenny Lau]

wait no

[Kenny Lau]

that isn't what I said

[Kenny Lau]

however given two explicit terms of type p_adic_integer -> nat, you can decide if they are equal. (This is a meta-theorem, not a theorem)

here

[Kenny Lau]

you gave me two terms of type p_adic_integer

[Mario Carneiro]

what is an explicit term of p_adic_integer? It is a lambda, which is a computable function

[Kenny Lau]

right

[Kenny Lau]

but I'm talking about terms which have type p_adic_integer -> nat

[Mario Carneiro]

oh you are using Andrej Bauer's trick

[Kenny Lau]

right

[Kenny Lau]

someone should make that a tactic :P

[Mario Carneiro]

well, it's still false because choice is an explicit term

[Kenny Lau]

constructive

[Tobias Grosser]

Here the interesting part:

Obviously there is no direct translation of concepts like linear inequalities and Barycentric Division to non-ordered fields, such as the p-adic ones. Nevertheless we want our p-adic polytopes and simplexes to be defined by conditions which are as simple as possible, to obtain a notion of faces satisfying all the above properties, and most of all to develop a flexible and powerful division tool. This is achieved here by first introducing and studying certain subsets of Γm called “largely continuous precells modN”, for a fixed m-tuple N of positive integers. These sets will be defined by a very special triangular system of linear inequalities and congruence relations modN. In particular they are defined simply by linear inequalities in the special case where N= (1,...,1) ...

[Tobias Grosser]

and

We extend the binary congruence relations of Z to Γ with the convention that a≡+∞[N] for every a∈Γ and everyN∈N. A subset A of FI(Γm) is a basic Presburger set if it is the set of solutions of finitely many linear inequalities and congruence relations. Although we will not use it, it is worth mentioning that, by the quantifier elimination of the theory of Z in the language LP res, the definable subsets of Z d, and more generally of Γm, are exactly the finite unions of basic Presburger sets.

[Tobias Grosser]

Need to allocate a weekend to go through the paper carefully before i can have an in-depth discussion here.

[Tobias Grosser]

Thanks for the comments.

[Mario Carneiro]

@Kenny Lau Here's a stab at your first statement: suppose P Is a program that decides equality for terms of type T. Given inputs (x, y), P will make some number of decisions (like if statements) before announcing true or false, which maps (x, y) in $\mathbb{Z}\subseteq\mathbb{Z}_2$ where the ones and zeros correspond to the choices, and the termination is because P always halts. This is a mapping $F : T \times T \to \mathbb{Z}$, and there is some set $S\subseteq \mathbb{Z}$ of "accepting states" where the program announces equality; correctness of P implies $F(x,y)\in S\iff x=y$.

If P has access to mysterious operations that measure x and y jointly, then it is possible that x=y is just a single instruction in the machine and so the theorem won't hold. Instead, we assume that each branching operation measures some property of either x or y but not both at the same time. (Stuff like comparing the first bit of x against the first bit of y can be split into two branches to measure first x then y.)

Now if $F(x,x) = F(y,y)$, meaning that the same sequence of operations that lead to the decision $x=x$ or $y=y$, then we also have $F(x,x)=F(x,y)$ because both execution paths make the same decisions regardless of whether they are examining $x$ or $y$. Thus $x=y$, so $F$ is injective on the diagonal and hence $T$ is countable.

[Rob Lewis]

Looks like I missed an interesting conversation, but just to answer the easy questions at the beginning! @Tobias Grosser indeed, referencing a git hash would be ugly but more stable. I'll try it out. The construction does require p to be prime. I don't even have a picture of what Presburger arithmetic over Z_p would look like since there's no ordering. Maybe there's an answer in the polytope paper you linked, that looks super interesting.

[Tobias Grosser]

Thanks @Rob Lewis for the answer. I would really like to discuss some of these topics in Freiburg.

[Tobias Grosser]

Need to do more reading to be able to have at least a somehow sensible conversation.

[Tobias Grosser]

Getting your opinion on this topic would be very useful.

[Rob Lewis]

For sure!

[Tobias Grosser]

Regarding the lack of ordering, in our compiler we associate to comparisions the information if a comparision should be interpreted as signed or unsigned.

[Tobias Grosser]

In this sense, hence there are two "order" relations.

[Tobias Grosser]

When when interpreting the values as signed integers, the other when interpreting them as unsigned.

[Tobias Grosser]

They are to my understanding not compatible.

[Tobias Grosser]

And maybe don't work for generic p-adic numbers, but just the finite bitwidth numbers we are interested in.

[Reid Barton]

They're also both not compatible with other structure like addition. For example if $a \ge b$ (in either sense), then it does not follow that $a + c \ge b + c$, unless you know that the additions do not overflow somehow

[Tobias Grosser]

Right.

[Reid Barton]

If you tried to define inequalities similarly for the 2-adics, then you should "start from the left-most bit"--but there is no left-most bit of a 2-adic number

[Tobias Grosser]

Right. Many things don't fully checkout here.

[Reid Barton]

I took a quick look at that paper and it was a bit hard to understand what their goal was, in part because the paper seemed to be setting up some background theory for a subsequent paper. But as far as I can tell, it talks about Presburger arithmetic not on Z_p or Q_p directly but on N or Z via the p-adic valuation.

[Reid Barton]

You could also say that Presburger arithmetic on N is really just the first order theory of addition (and zero) because an inequality $a \le b$ can be represented by $\exists c, a + c = b$. So then you could ask about the first order theory of addition for Z_p. I think it would just reduce to making statements about the p-adic valuations.

[Tobias Grosser]

Interesting.

[Siddharth Bhat]

@Reid Barton what does it mean to perform presburger arithmetic on the p-adic valuation?

[Reid Barton]

Well the p-adic valuation of a p-adic integer is a natural number, and Presburger arithmetic is the theory of natural numbers under zero and addition. So we're talking about formulas like "$v_p(x) = v_p(y) + v_p(y) + 1$".

[Siddharth Bhat]

Ah, hm.

[Siddharth Bhat]

@Reid Barton Do you know, how much of the geometry of presburger sets is left over when you move to p-adics?