Zulip Chat Archive

Stream: general

Topic: CPP paper


view this post on Zulip Rob Lewis (Oct 16 2018 at 08:54):

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!

view this post on Zulip Rob Lewis (Oct 16 2018 at 08:56):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 09:04):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 09:05):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 09:07):

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.

view this post on Zulip Johan Commelin (Oct 16 2018 at 09:08):

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 09:08):

Also, congrats with the draft :wink:

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 09:08):

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 :-)

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 09:12):

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.

view this post on Zulip Johan Commelin (Oct 16 2018 at 09:15):

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].)

view this post on Zulip Rob Lewis (Oct 16 2018 at 09:16):

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!

view this post on Zulip Rob Lewis (Oct 16 2018 at 09:16):

@Johan Commelin Thanks, fixed :slight_smile:

view this post on Zulip Rob Lewis (Oct 16 2018 at 09:17):

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.

view this post on Zulip Rob Lewis (Oct 16 2018 at 09:18):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 12:00):

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.

view this post on Zulip Rob Lewis (Oct 16 2018 at 12:11):

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.

view this post on Zulip Rob Lewis (Oct 16 2018 at 12:13):

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.

view this post on Zulip Rob Lewis (Oct 16 2018 at 12:16):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 12:17):

Thanks so much for the algorithm Rob!

view this post on Zulip Rob Lewis (Oct 16 2018 at 12:18):

Just remember it isn't a decision procedure!

view this post on Zulip Tobias Grosser (Oct 16 2018 at 15:58):

Very nice!

view this post on Zulip Tobias Grosser (Oct 16 2018 at 15:58):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:02):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:02):

Put it already on my reading list.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:03):

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?"

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:04):

Does your representation require p to be prime?

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:05):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:06):

nothing uncountable can be decidable

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:07):

OK, I need to understand this in more detail.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:08):

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.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:09):

I am not sure what the delta is in between.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:16):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:16):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:18):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:19):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:21):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:21):

that would be like doing real numbers to 32 significant figures

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:22):

Right.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:22):

That should then be trivially decidable, afaiu.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:22):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:23):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:24):

I see.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:25):

AFAIU Z/2^n Z gives just positive numbers

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:25):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:26):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:27):

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.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:28):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:28):

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 16:29):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:30):

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, ...)

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:30):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:31):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:31):

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.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:31):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:31):

but a dense set :P

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:31):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:32):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:32):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:32):

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.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:33):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:33):

This is hopeless.

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:34):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:34):

I see.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:34):

Thanks @Mario Carneiro for explaining this.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:34):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:35):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:35):

There's no inequalities either, if you need inequalities

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:35):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:36):

nothing uncountable can be decidable

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:36):

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)

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:36):

nothing uncountable can be decidable

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

that's a meta-theorem as well

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:36):

false

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:37):

hmm?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:37):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:38):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:38):

even so

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:38):

i.e. computable functions

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:38):

@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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:38):

computable number equality is not decidable

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:38):

even though it is a countable set

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:39):

so the converse of your statement is false

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:39):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:39):

that won't be a computable function

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:39):

that's a computable function

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:39):

ah wait

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:39):

termination in n steps is decidable

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:40):

wait no

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:40):

that isn't what I said

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:40):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:40):

you gave me two terms of type p_adic_integer

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:41):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:42):

right

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:42):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:42):

oh you are using Andrej Bauer's trick

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:42):

right

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:42):

someone should make that a tactic :P

view this post on Zulip Mario Carneiro (Oct 16 2018 at 16:43):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:43):

constructive

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:57):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 16:58):

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.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 17:00):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 17:00):

Thanks for the comments.

view this post on Zulip Mario Carneiro (Oct 16 2018 at 17:35):

@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 ZZ2\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×TZF : T \times T \to \mathbb{Z}, and there is some set SZS\subseteq \mathbb{Z} of "accepting states" where the program announces equality; correctness of P implies F(x,y)Sx=yF(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)F(x,x) = F(y,y), meaning that the same sequence of operations that lead to the decision x=xx=x or y=yy=y, then we also have F(x,x)=F(x,y)F(x,x)=F(x,y) because both execution paths make the same decisions regardless of whether they are examining xx or yy. Thus x=yx=y, so FF is injective on the diagonal and hence TT is countable.

view this post on Zulip Rob Lewis (Oct 16 2018 at 18:57):

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.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 18:59):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 18:59):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 18:59):

Getting your opinion on this topic would be very useful.

view this post on Zulip Rob Lewis (Oct 16 2018 at 19:00):

For sure!

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:01):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:02):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:02):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:02):

They are to my understanding not compatible.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:03):

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

view this post on Zulip Reid Barton (Oct 16 2018 at 19:03):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:04):

Right.

view this post on Zulip Reid Barton (Oct 16 2018 at 19:05):

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

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:05):

Right. Many things don't fully checkout here.

view this post on Zulip Reid Barton (Oct 16 2018 at 19:06):

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.

view this post on Zulip Reid Barton (Oct 16 2018 at 19:08):

You could also say that Presburger arithmetic on N is really just the first order theory of addition (and zero) because an inequality aba \le b can be represented by c,a+c=b\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.

view this post on Zulip Tobias Grosser (Oct 16 2018 at 19:12):

Interesting.

view this post on Zulip Siddharth Bhat (Oct 21 2018 at 18:39):

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

view this post on Zulip Reid Barton (Oct 21 2018 at 18:42):

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 "vp(x)=vp(y)+vp(y)+1v_p(x) = v_p(y) + v_p(y) + 1".

view this post on Zulip Siddharth Bhat (Oct 21 2018 at 18:47):

Ah, hm.

view this post on Zulip Siddharth Bhat (Oct 21 2018 at 18:53):

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


Last updated: May 17 2021 at 22:15 UTC