Rationals needed for the Frac CMRA?

Stream: iris-lean

[Shreyas Srinivas]

Based on my reading of the Frac CMRA, we need rational numbers to define it. Currently Rationals are defined in batteries. Should we include batteries as a dependency?

[Shreyas Srinivas]

CC : @Mario Carneiro and @Markus de Medeiros

[Shreyas Srinivas]

When we used iris in my semantics course we used it with stdpp and batteries serves a similar role in lean (but has some content differences), so hopefully it isn't a controversial addition

[Markus de Medeiros]

To port this file you don't actually need the rationals! This is a case where we can generalize the existing Iris implementation to require a typeclass with the properties we want, rather than the Rational type itself (namely, a type of positive numbers). I'll push my implementation of Frac in an hour or so.

[Markus de Medeiros]

Adding batteries is a bit of an orthogonal issue to this (though I'm definitely not be opposed to adding it when the need arises!)

[Shreyas Srinivas]

Ah okay. I actually want to get a hang of CMRAs (I only learnt the simplified resource algebra story in my course)

[Mario Carneiro]

presumably a minimalistic type which serves the role here would actually be dyadic rationals

[Shreyas Srinivas]

So I think I can try the Frac CMRA or some variant, just as a practice. Feel free to close the PR if you prefer it

[Markus de Medeiros]

It would be better to use a typeclass. I am sure that eventually I will want to instantiate this with the positive reals.

[Shreyas Srinivas]

what exactly is a Leibniz structure?

[Shreyas Srinivas]

conceptually?

[Mario Carneiro]

Leibniz equality is Rocq-speak for Eq

[Mario Carneiro]

I'm quite dubious about using the terminology in iris-lean since no one uses it here

[Mario Carneiro]

A Leibniz OFE is one where the Equiv relation is Eq

[Shreyas Srinivas]

some possibly mixed up questions : Equivalence is in Init. Why isn't Equivalence Eq defined in core?

[Shreyas Srinivas]

and why do we use this extra indirection in Iris at the moment?

[Mario Carneiro]

what indirection?

[Shreyas Srinivas]

structure LeibnizO (T : Type _) where
  car : T

-- Move?
theorem Eq_Equivalence {T : Type _} : Equivalence (@Eq T) :=
  ⟨congrFun rfl, (Eq.symm ·), (· ▸ ·)⟩

instance : COFE (LeibnizO T) := COFE.ofDiscrete _ Eq_Equivalence

[Mario Carneiro]

LeibnizO is a type constructor which builds a COFE on an arbitrary type, which is also a leibniz OFE

[Mario Carneiro]

You don't want that structure on every type, it's like the discrete topology

[Markus de Medeiros]

Are there any rules about when we should use indirection? I brought up the fact that we put the discrete function CMRA on every function type but I don't think that point was ever resolved.

[Mario Carneiro]

The key question is whether there is a likelihood of conflict between different structures

[Mario Carneiro]

For function types, it's fine as long as you can argue that there will never be a different structure on function types (only wrapped function types)

[Mario Carneiro]

for LeibnizO this is clearly impossible to argue because it would be a blanket instance covering every type

[Markus de Medeiros]

Mario Carneiro said:

only wrapped function types

Ah--good point. I'm not sure I've ever seen a function type in Iris that wasn't wrapped into a discrete function with -d>.

[Markus de Medeiros]

So it might as well be the default

[Mario Carneiro]

I believe there is no competing instance for function types anyway; -n> isn't a function type, it is a subtype of a function type

[Shreyas Srinivas]

Also @Markus : there seems to be no clean way to map arbitrary typeclass instances from Fractional to Frac

[Shreyas Srinivas]

Referring to this part:

abbrev Frac (T : Type _) [Fractional T] := LeibnizO T

-- TODO: How do I get rid of these instances?
-- I definitely do not want to use an abbrev for Frac (there are many different OFE's for numerical types)
-- so do we need to keep around all of these coercions?
instance [Fractional T] : Coe (Frac T) T := ⟨(·.1)⟩
instance [Fractional T] : Coe T (Frac T) := ⟨(⟨·⟩)⟩
@[simp] instance [Fractional T] : COFE (Frac T) := by unfold Frac; infer_instance
@[simp] instance [Fractional T] : One (Frac T) := ⟨⟨One.one⟩⟩
@[simp] instance [Fractional T] : LE (Frac T) := ⟨fun x y => x.1 ≤ y.1⟩
@[simp] instance [Fractional T] : LT (Frac T) := ⟨fun x y => x.1 < y.1⟩
@[simp] instance [Fractional T] : Add (Frac T) := ⟨fun x y => x.1 + y.1⟩

[Shreyas Srinivas]

I made a draft PR to your PR at leanprover-community/iris-lean#57

[Shreyas Srinivas]

I want to simplify this further tomorrow morning

[Shreyas Srinivas]

For example, I think the positivity condition is pointless

[Shreyas Srinivas]

Since we are focussed on positive numbers only, we could add define the four conditions of Fractional in simpler terms. However changes here will break proofs, so I will fix this after some sleep

[Markus de Medeiros]

Nice! Yeah feel free to play around with it, I didn't simplify the Fractional typeclass at all :)

[Markus de Medeiros]

I do think positivity will be hard to remove (the type in Rocq is actually the positive rationals in case you missed it!)

[Shreyas Srinivas]

To clarify I mean we can take positivity simpler

[Shreyas Srinivas]

Trying to simplify positivity has had the side effect of creating a lot of useful API lemmas for the Fractional class

[Markus de Medeiros]

Your definition looks nice! Is it minimal?

[Shreyas Srinivas]

I don't have a proof of that. I am trying to codify rationals as totally ordered commutative monoids (ignoring multiplication).

[Shreyas Srinivas]

I am basically remembering Apostol's definition of ordered fields in his real analysis book and simply removing the multiplication axioms. I don't have a copy so I have to go with my memory

[Markus de Medeiros]

Okay! We don't need a proof or anything, just want to be reasonably confident that this typeclass is as minimal as possible.

[Shreyas Srinivas]

I have marked a couple of the remaining fields for removal after I prove them as theorems

[Shreyas Srinivas]

Oh and I miss quite a few tactics I take for granted in mathlib like contrapose, apply .. at, nth_rw, and simp_rw

[Markus de Medeiros]

I pushed iris-lean#59, we'll want Fractional to be the smallest typeclass such that everything in DFractional can also be proved.

[Markus de Medeiros]

Uh also, I think you should not use Zero. This cannot be instantiated for types that are intrinsically positive like the positive reals or positive rationals.

[Shreyas Srinivas]

Okay, but then the class that comes out of it will not be a monoid

[Markus de Medeiros]

That's fine

[Shreyas Srinivas]

I also miss all those precious code actions that split cases and create proof holes

[Shreyas Srinivas]

Everywhere you see me using the conv mode, I would have used nth_rw instead.

[Shreyas Srinivas]

Btw the Zero class only adds the notation for zero. For various intervals of Q I think the correct way to do this is by adding properties with the upper and lower bounds

[Shreyas Srinivas]

So I think the zero and id laws should remain

[Shreyas Srinivas]

And then this Fractional class should be extended with another that bounds the valid range of values. Kinda like subtypes

[Shreyas Srinivas]

Otherwise the order relations’ compatibility with addition will become complicated. Further, we would have to reinvent many of the API lemmas I have already proved

[Mario Carneiro]

Shreyas Srinivas said:

I also miss all those precious code actions that split cases and create proof holes

Those are in Batteries

[Markus de Medeiros]

Shreyas Srinivas said:

Btw the Zero class only adds the notation for zero. For various intervals of Q I think the correct way to do this is by adding properties with the upper and lower bounds

There is no zero in the positive rationals.

[Shreyas Srinivas]

Yeah but for positive rationals you can restrict the allowed values using a property

[Markus de Medeiros]

I understand that mechanizing a monoid is easy but that is not the structure we want. If the type includes zero elements we will need to change the CMRA to accommodate this, but since this is CMRA is used extensively throughout the derived parts of Iris I am hesitant to do that.

[Shreyas Srinivas]

I would call it “PositiveFractional” and impose a restriction that all values a strictly greater than 0

[Markus de Medeiros]

...PositiveFractional cannot extend zero then.

[Shreyas Srinivas]

0 won’t be a valid value if PositiveFractional

[Shreyas Srinivas]

Only fractional

[Shreyas Srinivas]

0 will be ruled out by the inability to prove the strict positivity field

[Shreyas Srinivas]

It’s basically like docs#Subtype

[Markus de Medeiros]

The stuff you've done is great, and it will be convenient to say that the positive restrictions of the classes you laid out will be PositiveFractional! But PositiveFractional itself should be a typeclass.

Think of how you would instantiate PositiveFractional for the type of intrinsically positive fractions represented as pairs structure PFrac : {num : Nat+; den: Nat+; wf : gcd num den = 1}. Under your strategy, you would have to add a zero onto this type

inductive positiveFracPlusZero
| pos : PFrac
| zero

then lift all of the PFrac operations to positiveFracPlusZero, all to use {p : positiveFracPlusZero | 0 < p} as the type of your indices. This is a mess.

[Shreyas Srinivas]

Once I’m back I’ll flesh it out in code.

[Shreyas Srinivas]

Maybe it will be easier to communicate it that way

[Shreyas Srinivas]

In a way you are right. But we can add default tactic arguments like by omega to make most of the api seamless

[Shreyas Srinivas]

And then we just establish the API with general bound parameters. EDIT: this is how docs#Vector works on top of docs#Array

[suhr]

By the way, why do we need rationals for program verification?

[suhr]

(sorry if the question is silly, I do not have that much experience with Iris)

[Shreyas Srinivas]

Yeah. This cmra expresses fractional ownership later

[Mario Carneiro]

So fractions come up in "fractional ownership" which are a way of dealing with avoiding races between readers and writers. Let's say we want to ensure the property:

• A writer can only write if there are no concurrent readers or writers
• Multiple readers can read concurrently

To accomplish this, we can have a separating proposition $\ell\mapsto_1 v$ which represents full ownership of the value, and if you have this then you are the unique owner and can safely write. If you want to share read access to it, you can "split" the ownership into two pieces, $(\ell\mapsto_{1/2} v)\ast (\ell\mapsto_{1/2} v)$, and now distribute these pieces to separate threads of execution. If you have only half of a permission, then you do not know that there are no concurrent readers so you are entitled only to read the value, not write it. The reason for having arbitrary rationals is so that these tokens can be arbitrarily split and passed around, and you can keep reading it as long as the fraction remains positive. When all is done you can recombine the pieces into one full permission and go back to writing.

[Mario Carneiro]

Here is what I would expect from an axiomatization of the type of positive fractions here, with the model $(0,1]$ in mind:

• $1$ is a permission
• $a+b=c$ is a functional ternary relation on permissions (write $a+b$ when this exists)
• $(a+b)+c=a+(b+c)$
• $a+b=b+a$
• $a/2$ is a function such that $a/2+a/2=a$

I think that's it?

[Shreyas Srinivas]

I think Markus wants something more general. He mentioned wanting to use Real number intervals later

[Markus de Medeiros]

Adding onto Mario's explanation, the problem with a zero fraction  $\ell\mapsto_0 v$ is that it _does not_ denote read permissions to a location, so it adds an edge case that needs to be handled by the validity predicate of the CMRA.

[Shreyas Srinivas]

But yeah I am still convinced that a dual api with default arguments and/or partial functions is the way to handle bounded fractions.

[Shreyas Srinivas]

Same as Array and Vector

[Shreyas Srinivas]

Otherwise we lose substantially simplicity of API

[Mario Carneiro]

note that all of the following satisfy my axioms:

• $(0,1]$
• $\mathbb{Q}\cap(0,1]$
• $\mathbb{D}\cap(0,1]$, $\mathbb{D}$ = dyadic rationals
• $\mathbb{R}^+$
• $\mathbb{Q}^+$
• $\mathbb{D}^+$

You can only concretely construct fractions in $\mathbb{D}\cap(0,1]$ as literals though.

[Markus de Medeiros]

That's right. I'm not convinced that your axiomatization actually has everything needed to instantiate CMRA (you don't have a relationship between addition and 1, for example) and the division by 2 axiom is useless.

[Mario Carneiro]

To construct 3/4 you need an axiom saying that when $a+(b+c)$ exists, $a+b$ also exists and $a+(b+c)=(a+b)+c$ (this is the associativity axiom but more precise about what exists)

[Mario Carneiro]

The division by 2 axiom is certainly not useless, it's the only way you can actually make fractions

[Markus de Medeiros]

Useless for the CMRA instance, which is what were talking about.

[Mario Carneiro]

otherwise $\{1\}$ would also be a model of the axioms

[suhr]

You also need a ≠ a/2.

[Mario Carneiro]

why?

[Markus de Medeiros]

Mario Carneiro said:

otherwise $\{1\}$ would also be a model of the axioms

$\{1\}$ is fine!

[Mario Carneiro]

is $\mathbb{R}^+$ fine?

[Markus de Medeiros]

Yes.

[Markus de Medeiros]

Oh-- actually {1} is not fine, sorry. You need addition.

[Mario Carneiro]

no you have addition, it's just an empty relation in my setting

[Mario Carneiro]

so you can talk about splitting but you can never actually do it

[Markus de Medeiros]

I suppose you could change Add to be a relation instead of a function, yes. Then {1} is fine.

[Markus de Medeiros]

Frac {1} is the same as Excl I believe.

[Mario Carneiro]

I use a relation because I expect that the CMRA wants to do this PCM style

[Mario Carneiro]

so we have this way of combining values which is just not always defined

[Markus de Medeiros]

The well-definition is already controlled by the validity predicate of the CMRA

[Mario Carneiro]

if we restrict to those sets which have 1 as an upper bound then we get the relation $a+1=b\to\bot$ which is nice

[Markus de Medeiros]

I could believe that. The question then becomes if using a relation instead of a function is easier for clients.

[Markus de Medeiros]

Is there (rational/real/natural) addition defined as a relation somewhere? I only know of it defined as a function.

[Mario Carneiro]

You can define $a<b$ as $\exists c,c+a=b$ (which works also when 1 is not an upper bound) and then $\neg a<1$ means that you can write

[suhr]

Anyway, speaking of axioms, what stops defining + in a trivial way: 1 + 1 = 1, where 1 is only value of the type?

This should satisfy the axioms?

[Mario Carneiro]

and you want an axiom $\neg a<a$

[Mario Carneiro]

which will prevent your example @suhr

[Markus de Medeiros]

Concretely, this is not sound from a logical perspective. You can't exchange $\ell\mapsto_1 v$ for $\ell\mapsto_1 v \ast \ell\mapsto_1 v$ because then you get two write permissions to the same place.

[Mario Carneiro]

right, but the question is whether this should be prevented in the axioms somehow so that you can actually prove a soundness theorem for generalized fractional permissions using this typeclass

[Mario Carneiro]

there is a bit of difference between the sets that have 1 as an upper bound (which prefer the partial addition version) and those that are unbounded (which can have addition as a function but need more side conditions saying things are less than 1)

[Mario Carneiro]

What is the type actually used in iris for this?

[Markus de Medeiros]

Just to bring the discussion back down to earth, Iris does the following:

• Use a function for fraction addition
• Internalize that the fraction values are positive
• Externalize that the fraction values are at most 1 (using the CMRA validity predicate)

Iris uses Qp, the type of positive rationals for this.

[Mario Carneiro]

is division used?

[Markus de Medeiros]

Not for the CMRA instance

[Markus de Medeiros]

The generalization I'm suggesting matches Iris in terms of externalizing/internalizing different features of Qp, but generalizes the Qp type itself. Other generalizations are possible, but may change the derived proofs in tricky ways.

[Mario Carneiro]

in that case how about this:

• $1$ exists
• $a+b$ exists
• $a+b=b+a$, $(a+b)+c=a+(b+c)$
• define $a<b$ as $\exists c,c+a=b$, define $a\le b$ as $\neg b<a$
• $a\le a$

[Mario Carneiro]

there is no explicit relationship between 1 and + but you would use $a\le 1$ in the validity predicate

[Markus de Medeiros]

Mario just for context you can look at the Fractional class in my PR to see a sufficient set of axioms. @Shreyas Srinivas it's worth a shot to try reducing my typeclass to Mario's axioms.

[Markus de Medeiros]

Mario Carneiro said:

there is no explicit relationship between 1 and + but you would use $a\le 1$ in the validity predicate

Right, I get it. I did use the field one_strict_max in my DFractional typeclass (which Fractional should also subsume) but I feel that may be able to be removed.

[Mario Carneiro]

You should be able to prove transitivity of $<$ and $\le$ using associativity

[Mario Carneiro]

oh we do need to add $c+a=c+b\to a=b$

[Mario Carneiro]

le_refl and positive are the same thing if you have $a\le b\leftrightarrow\neg b<a$

[Mario Carneiro]

and so add_le_mono should be provable

[Mario Carneiro]

(Just to be clear, I'm approving of the general structure of @Markus de Medeiros 's PR, this should be a custom typeclass.)

[Mario Carneiro]

the details of the axioms aren't too important

[Markus de Medeiros]

Your axiom "$a+b$ exists" means that we should keep + as a function (as it is now) instead of a relation, right? This detail does matter for the downstream code I am working on.

[Mario Carneiro]

yes

[Mario Carneiro]

this does mean that we won't be able to support $\mathbb{D}\cap (0,1]$ as a model; there is no way you can do addition as a function without saturating, which violates cancellativity

[Mario Carneiro]

it also means 1 + 1 = 1 which violates irreflexivity

[Markus de Medeiros]

Hm. What is  $\mathbb{D}$ in this context?

[Mario Carneiro]

dyadic rationals

[Mario Carneiro]

$\mathbb{R}$ and $\mathbb{Q}$ also have the same behavior though

[Markus de Medeiros]

Ah right--the issue is the $$...\cap (0,1]$$ part.

[Shreyas Srinivas]

There seems to be a lot of messages here. What’s the conclusion?

[Markus de Medeiros]

• You should try and refine the type class on my initial PR (without a Zero instance), Mario's axioms are probably the refinement you want
• Your work (the classes with a Zero instance) can stay, the positive subtype of them can be used as a generic instance for the Fractional typeclass

[Markus de Medeiros]

• The Fractional typeclass you end up with should subsume both Fractional from the frac branch and DFractional from the DFrac branch.

[Shreyas Srinivas]

My work is a bit generic. It just happens to subsume Fractional. Since Fractional is meant to use a different axiom set, should I move my work to a separate file? Alternatively, I can understand point 2 to mean that you wish to have all the API lemmas and properties from the typeclass, but have them proved from these axioms.

[Markus de Medeiros]

Where you put your work or if you keep it is largely irrelevant, just give it a shot (if you still want to!) and let me know when you're done so I can review it and give more detailed feedback.

[Shreyas Srinivas]

Okay. I’ll do this tomorrow. It’s past midnight in my time zone.

[Shreyas Srinivas]

Fwiw, the APi lemmas I showed for this typeclass will also be needed to make Mario’s definitions usable downstream.

[Shreyas Srinivas]

We are basically foregoing all the order theory and algebra that was developed for mathlib. So we need to recover the basic properties that a mathlib user can take for granted.

[Mario Carneiro]

I think that's the wrong way to look at it. As suhr remarked, it's surprising that we need rational numbers to begin with, and the truth is that we don't really, we need an extremely basic structure of which rational numbers are the simplest to explain model. Generalizing to the minimum properties necessary actually makes it clearer what's actually going on, and reveals that this really has little to do with rational numbers or any of their algebraic properties.

I am reminded of the evolution of "the interval" in HoTT and cubical type theory. Once upon a time people did homotopy theory using the type $[0,1]\subseteq \mathbb{R}$, which captures a bunch of structure of topological spaces. But when going synthetic, people started to realize that they can get away with just a rational interval and they get something computable, and in modern cubical type theory it's an extremely basic type, like "thing that has a 0 and 1 and maybe $\max$?" And keeping things to that minimal subset is exactly what makes it possible to have a decidable theory of equality, which is part of what makes cubical type theory possible.

[Shreyas Srinivas]

hmm.. In neural nets, researchers went from all sorts of non-linear functions like the sigmoid function to softmax for the threshold

[Shreyas Srinivas]

I see your point. But I just realised that my generalisation also captures the $(\N, +)$ resource for counters I had in my course. Except their core is the constant function $0$. EDIT : It also captures $(\N, max)$

[Shreyas Srinivas]

For now I will use your axioms in the Frac CMRA, but keep the PR for the stuff I wrote open

[Mario Carneiro]

Shreyas Srinivas said:

I see your point. But I just realised that my generalisation also captures the $(\N, +)$ resource for counters I had in my course. Except their core is the constant function $0$

I think that's a different use case, which uses a monoid

[Shreyas Srinivas]

It's a commutative monoid with a total order. EDIT : Both $(\N, +)$ and $(\N, max)$

[Shreyas Srinivas]

Screenshot from 2025-06-24 02-21-15.png

[Markus de Medeiros]

Yes, commutative monoids can be a resource (you should do the numbers resources after this!) But these are different than Frac. It is essential that Frac have a maximum valid element which neither (Nat, +) nor (Nat, max) really do.

[Shreyas Srinivas]

Okay. In that case I will proceed as follows:

1. I will move my current Frac.lean to Numbers.lean. Maybe even rename the PR.

[Shreyas Srinivas]

2. Separately start a new PR against your PR to add the axioms Mario suggested for Frac.lean

All this tomorrow

[Shreyas Srinivas]

Mild confusion. In Init.Prelude online, I see a typeclass One here

[Shreyas Srinivas]

But somehow I can't access this in iris-lean

[Shreyas Srinivas]

Did something change between toolchain updates?

[Shreyas Srinivas]

This is the same part of the same file but opened in my editor with Ctrl + Click and the One typeclass is missing

Screenshot from 2025-06-25 13-55-15.png

[Oliver Soeser]

That typeclass was only added two months ago, maybe the version of Lean you're using doesn't have it yet?

[Shreyas Srinivas]

Okay that's possible. I haven't merged master and I don't think Markus has either

[Shreyas Srinivas]

I remember this class being around for a while.

[Oliver Soeser]

That typeclass has certainly been around for a while, but I think it was scattered across different files

[Shreyas Srinivas]

Nah it isn't there even in v4.20.0

[Oliver Soeser]

This seems to be the commit that brought it into the Prelude: # Commit 196d899

[Shreyas Srinivas]

Then it is surprising that it wasn't in this month's release

[Oliver Soeser]

Are you sure you're running v4.20? One is in the Prelude for me: image.png

[Shreyas Srinivas]

Oh thanks. I was in the wrong branch

[Oliver Soeser]

No worries!

[Shreyas Srinivas]

We need totality of the order relation

[Oliver Soeser]

What requires that?

[Shreyas Srinivas]

You can't prove it from the axioms above

[Shreyas Srinivas]

But maybe I am thinking about this the wrong way.

[Shreyas Srinivas]

Maybe we don't need to prove it

[Oliver Soeser]

Mario Carneiro said:

in that case how about this:

• $1$ exists
• $a+b$ exists
• $a+b=b+a$, $(a+b)+c=a+(b+c)$
• define $a<b$ as $\exists c,c+a=b$, define $a\le b$ as $\neg b<a$
• $a\le a$

These axioms?

[Shreyas Srinivas]

leanprover-community/iris-lean#62

[Kevin Buzzard]

FWIW $(\Z_{>0})^2$ (with 1 defined arbitrarily and + defined componentwise) seems to satisfy the both the axioms quoted by Oliver and the ones in the PR, and isn't total.

[Shreyas Srinivas]

I am beginning to think the only thing that we really need to check is if $x < 1$ for some $x$

[Shreyas Srinivas]

If not, then $x = 1$ and we have total ownership of some resource

[Shreyas Srinivas]

More concretely, total ordering is not necessary

[Markus de Medeiros]

That's an interesting thought

[Oliver Soeser]

That's my intuition too, totality seems like an unnecessary restriction

[Markus de Medeiros]

It would be cool if we could instantiate it with abstract fractional permissions like here (though I wouldn't read too much into their exact permissions structure itself)

[Shreyas Srinivas]

Lol. I was thinking of something just like that

[Shreyas Srinivas]

Basically you don't need any operation other than halving and recombining

[Shreyas Srinivas]

there is an implicit partial order in halving

[Shreyas Srinivas]

So we only combine things that are equal in this order

[Shreyas Srinivas]

what we really need is an abstract binary tree structure where leaf nodes at the same level can be combined into a leaf node at the parent level or split

[Markus de Medeiros]

DFrac is more like the abstract fractional permissions in that paper, and deals with the invalid combinations, I think? Would be interesting to see if generalizing to partial orders (with total comparisons to 1) could simplify these OFE's.

[Markus de Medeiros]

Shreyas Srinivas said:

what we really need is an abstract binary tree structure where leaf nodes at the same level can be combined into a leaf node at the parent level or split

The rationals are not a binary tree so this is not right.

[Shreyas Srinivas]

no they are not, but as Mario says, we just need dyadic rationals

[Oliver Soeser]

I don't see why we can only combine equals?

[Shreyas Srinivas]

It means we don't have to keep track of what we are adding

[Shreyas Srinivas]

two equal leaf child nodes yield a new leaf node at the parent level

[suhr]

The rationals are not a binary tree so this is not right.

SternBrocotTree.svg.png

[Oliver Soeser]

Would that still work in practice though? To my knowledge it's fairly common for unequal fractional permissions to be combined

[Shreyas Srinivas]

So let's take a step back and consider what the fractional ownership actually represents

[Shreyas Srinivas]

In terms of heaplang, we get to create two threads out of one, if we fork at a thread.

[Shreyas Srinivas]

we recombine ownership when we join two threads

[suhr]

One could also spawn N threads simultaneously and then somehow use the fact that threads are essentially the same?

[Shreyas Srinivas]

You can model that general scenario using dyadic rationals

[Shreyas Srinivas]

but the model that I think Mario has in mind is based on what we do in heaplang

[suhr]

You can, but the proof might become more complex.

[Shreyas Srinivas]

We can instantiate the class with rationals

[Shreyas Srinivas]

and define the combining operation in terms of addition

[Shreyas Srinivas]

We will have the issue you speak of in any case @suhr : The definition Mario proposed is rather general

[Shreyas Srinivas]

The creation of n threads is an atomic sequence of (n-1) forks

[Markus de Medeiros]

Yes. Halving of any kind is not necessary for the proof that Frac is a CMRA and therefore should not be part of the Fractional class.

[Shreyas Srinivas]

Anyway, I think I have most of it nailed. I only made two changes. I added an axiom that a < b -> a \neq b

[Shreyas Srinivas]

and defined a \leq b as a < b \or a = b

[Shreyas Srinivas]

This is much more convenient for proofs

[Markus de Medeiros]

Shreyas Srinivas said:

I am beginning to think the only thing that we really need to check is if $x < 1$ for some $x$

Just curious, did this not end up working out for some reason?

[Shreyas Srinivas]

Oh no it works. I didn’t imagine this PR was the right place to experiment since Mario and you already had a plan.

[Shreyas Srinivas]

In general I think frac should just be a rooted tree

[Shreyas Srinivas]

The arity need not be fixed

[Shreyas Srinivas]

Basically it would model thread ownership

[Markus de Medeiros]

Shreyas Srinivas said:

Oh no it works. I didn’t imagine this PR was the right place to experiment since Mario and you already had a plan.

Good to know!

[Shreyas Srinivas]

A thread can only return fractional ownership to its creator if it has the entirety of its piece. When a thread spawns with split ownership, then, correspondingly many child nodes are tacked on. When the child nodes return their piece they are deleted. Ownership is 1 only if the tree has a root node with no children.

Frac is a very special case of this where, we always maintain a version of the tree flattened upto the root node plus its children nodes :
meaning either of the following :

1. only the root node produces more pieces of partial ownership (or)
2. The only non root nodes are leaf nodes, which are children of the root. Instead of adding child nodes to a non root node, we simply replace that node with more leaf nodes.

In either case total ownership is represented by a tree with only the root node.

[Shreyas Srinivas]

The nice thing is one can effectively compute when ownership is complete without the imprecision of machine arithmetic or overhead of rational arithmetic.

[Shreyas Srinivas]

One can also precisely reason about when a thread can relinquish ownership of its fraction.

[Mario Carneiro]

Markus de Medeiros said:

Yes. Halving of any kind is not necessary for the proof that Frac is a CMRA and therefore should not be part of the Fractional class.

While true, I think you will probably want a class that extends this which actually contains a halving or similar operation, since without halving you can't actually do anything interesting with the class that would motivate including this CMRA in your iProp. And you might want to reconsider calling this class Fractional as there is nothing fractional about it, PNat satisfies the definition

[Mario Carneiro]

Shreyas Srinivas said:

In general I think frac should just be a rooted tree

That doesn't sound associative

[Mario Carneiro]

Shreyas Srinivas said:

A thread can only return fractional ownership to its creator if it has the entirety of its piece. When a thread spawns with split ownership, then, correspondingly many child nodes are tacked on. When the child nodes return their piece they are deleted. Ownership is 1 only if the tree has a root node with no children.

Your model, where you only recombine elements at the same height, is more restrictive than the actual fractional permissions model over Q, which in particular lets you do the following:

• Initialize with $x\mapsto_1 v$
• Split $x\mapsto_1 v$ into $(x\mapsto_a v)\ast (x\mapsto_b v)$ where $a+b=1$
• Fork off thread A with $x\mapsto_a v$ permission
• Split $x\mapsto_b v$ into $(x\mapsto_c v)\ast (x\mapsto_d v)$ where $c+d=b$
• Fork off thread C with $x\mapsto_c v$ permission
• Thread C passes its ownership of $x\mapsto_c v$ to thread A (say, through a mutex) and exits
• Thread A recombines permissions to $x\mapsto_e v$ where $a+c=e$
• Thread A dies and returns its permissions to main thread
• Main thread recombines permissions to $x\mapsto_1 v$ where $d+e=1$

If you keep track of what is happening with the fractions, you will see that at least one of the splits/merges $a+b=1$, $c+d=b$, $a+c=e$, $d+e=1$ has to involve adding two fractions that are not at the same height. Permitting splits and merges only in perfect halves only permits stack-like usage of read permissions and would ban the cross cut here where thread C passes its permission over to thread A.

[Shreyas Srinivas]

Okay but you can recover this by allowing child nodes to be transferred

[Shreyas Srinivas]

At that point that fractional piece (c) is shifted to a different subtree so the subtree rooted at (b) is not concerned about it

[Mario Carneiro]

my point is that you need associativity to hold, and it doesn't if you only allow combining equal pieces

[Mario Carneiro]

if we suppose that all the splits are equal, then $a=b=1/2$, $c=d=1/4$, and then $e=3/4$ and $1/4+3/4=1$ is an unequal merge

[Mario Carneiro]

that is, you need dyadic rationals, not just $\{1/2^n\mid n\in\mathbb{N}\}$

[Shreyas Srinivas]

Okay so concretely we need an operation that works on combining arbitrary subtrees associatively.

[Mario Carneiro]

what exactly are the trees you are referring to?

[Markus de Medeiros]

Mario Carneiro said:

While true, I think you will probably want a class that extends this which actually contains a halving or similar operation,

Yeah I wouldn't be opposed to this by any stretch! This won't affect anything beneath a program logic though, so it's library code.

[Mario Carneiro]

well you can't type a fork operation without it

[Markus de Medeiros]

Good thing the language I care about doesn't have fork :p

[Mario Carneiro]

why would you care about fractional permissions if you can't make fractions?

[Mario Carneiro]

we already have Auth, right?

[Markus de Medeiros]

Yes. But it's downstream of some constructions like gmap_view which I do care about.

[Markus de Medeiros]

In gmap_view the authoritative part has a fractional permission, and is used in a variety of program logics. We could write a version of gmap_view which elides this but it's nice that I can get the one I want without duplicating the structure.

[Markus de Medeiros]

It might be possible to parameterize gmap_view even further (parameterize the auth part by an arbitrary CMRA or something?) but I'm not sure about that yet.

[Markus de Medeiros]

Anyways, I ended up refactoring Shreyvas' code to implement his idea about comparing to 1

section Fractional
class Fractional (α : Type _) extends Add α where
  /-- Validity predicate on fractions. Generalizes the notion of `(· ≤ 1)` from rational fractions. -/
  proper : α → Prop
  add_comm : ∀ {a b : α}, a + b = b + a
  add_assoc : ∀ {a b c : α}, a + (b + c) = (a + b) + c
  add_left_cancel : ∀ {a b c : α}, a + b = a + c → b = c
  /-- There does not exist a zero fraction. -/
  add_ne : ∀{a b : α}, a ≠ b + a
  proper_add_mono_left : ∀ {a b : α}, proper (a + b) → proper a

/-- A type of fractions with a unique whole element. -/
class UFractional (α : Type _) extends Fractional α, One α where
  whole_iff_one {a : α} : whole a ↔ a = 1

section NumericFractional
/-- Generic fractional instance for types with comparison and 1 operators. -/
class NumericFractional (α : Type _) extends One α, Add α, LE α, LT α where
  add_comm : ∀ {a b : α}, a + b = b + a
  add_assoc : ∀ {a b c : α}, a + (b + c) = (a + b) + c
  add_left_cancel : ∀ {a b c : α}, a + b = a + c → b = c
  le_def : ∀ {a b : α}, a ≤ b ↔ a = b ∨ a < b
  lt_def : ∀ {a b : α}, a < b ↔ ∃ c : α, a + c = b
  lt_not_eq : ∀ {a b : α}, a < b → a ≠ b

instance [NumFractional α] : UFractional α where ...

I think UFractional is probably the most general class that doesn't cause real problems downstream, but I'll keep playing around with it over the next few days to find out.

[Mario Carneiro]

what is whole?

[Shreyas Srinivas]

I think it’s an implementation of the idea that the only order comparison you actually care about it with 1

[Mario Carneiro]

what is add_left_cancel used for?

[Mario Carneiro]

I thought that was proper @Shreyas Srinivas

[Mario Carneiro]

I don't think @Markus de Medeiros 's code compiles as written since whole isn't defined

[Shreyas Srinivas]

whole is proper when the order is total I suppose.

[Mario Carneiro]

no, whole appears to generalize a >= 1 while proper generalizes a <= 1

[Mario Carneiro]

or maybe 1 | a, I'm not sure because there are no axioms for it

[Markus de Medeiros]

Ah right--sorry I snipped that segment out of a couple parts of the PR. Here's the missing piece:

open Fractional in
/-- A fraction does not represent the entire resource.
Generalizes the notion of `(· < 1)` from rational fractions. -/
abbrev fractional [Fractional α] (a : α) : Prop :=
  proper a ∧ ∃ b, proper (a + b)

open Fractional in
/-- A fraction that is tne entire resource.
Generalizes the notion of `1` from rational fractions. -/
abbrev whole [Fractional α] (a : α) : Prop :=
  proper a ∧ ¬∃ b, proper (a + b)

[Mario Carneiro]

I would expect the first conjunct in fractional to not be needed

[Mario Carneiro]

FYI proper, fractional and whole should be capitalized

[Markus de Medeiros]

Proper generalizes <=, fractional generalizes <, whole generalizes 1. I wanted to see how general I could make the CMRA construction, but for some downstream code it is (or at least seems) important to have a unique whole element.

[Shreyas Srinivas]

Mario Carneiro said:

what is add_left_cancel used for?

I recall using it to prove a few lemmas about order in my pr to Markus’s PR

[Markus de Medeiros]

Mario Carneiro said:

I would expect the first conjunct in fractional to not be needed

I think you're right about that

[Mario Carneiro]

and if you do that then whole can be simplified using fractional

[Mario Carneiro]

these shouldn't be abbrevs

[Shreyas Srinivas]

The intuitive idea behind the tree is to represent how ownership of a resource is split. Each subtree represents the split up of some fragment of a resource. All currently owned resources are represented by leaf nodes. When a fragment of a resource is split (or some fragment taken out of the resource, the corresponding leaf node branches out into child nodes.

[Shreyas Srinivas]

These splits don’t have to be “equal”

[Shreyas Srinivas]

You might choose to transfer ownership of an entire subtree of resources to a different branch.

[Shreyas Srinivas]

I am trying to come up with the most free version of resource splitting that keeps track of the history of resource partitioning and sharing.

[Shreyas Srinivas]

One can also think of the internal & leaf nodes of the tree as threads, where only leaf threads hold resource fragments. When, say, a single thread is forked from another, the node of the parent thread splits into two child nodes of which one carries the resource of the newly forked thread, and the other carries what’s left in the parent thread. Conversely the join operation joins child nodes. If there are no other child threads left then a child node is merged into its parent node. If you wish to represent the transfer of resources to a different thread, this is done by attaching the corresponding subtrees as children of the node corresponding to the recipient thread.

[Shreyas Srinivas]

That being said, the more I write, the more complicated this seems to be getting. Rational numbers seem much simpler

[Mario Carneiro]

sure, you can imagine the resources as a finite antichain in the complete binary tree, but then the "numbers" need to represent sets of leaves, not just one

[Mario Carneiro]

and that's equivalent to dyadic rationals

[Mario Carneiro]

Actually if you really want the free structure defined by these axioms I think you would get:

inductive Rat where
  | one : Rat
  | left : Rat → Rat
  | right : Rat → Rat
  | add : Rat → Rat → Rat

inductive Equiv : Rat → Rat → Prop
  | refl : Equiv a a
  | symm : Equiv a b → Equiv b a
  | trans : Equiv a b → Equiv b c → Equiv a c
  | left : Equiv a a' → Equiv (.left a) (.left a')
  | right : Equiv a a' → Equiv (.right a) (.right a')
  | add : Equiv a a' → Equiv b b' → Equiv (.add a b) (.add a' b')
  | comm : Equiv (.add a b) (.add b a)
  | assoc : Equiv (.add a (.add b c)) (.add (.add a b) c)
  | split : Equiv (.add (.left a) (.right a)) a

inductive Disjoint : Rat → Rat → Prop
  | symm : Disjoint a b → Disjoint b a
  | split : Disjoint (.left a) (.right a)
  | left : Disjoint a b → Disjoint a (.left b)
  | right : Disjoint a b → Disjoint a (.right b)
  | add : Disjoint a b → Disjoint a c → Disjoint a (.add b c)
  | equiv : Equiv b b' → Disjoint a b → Disjoint a b'

inductive Valid : Rat → Prop
  | one : Valid .one
  | left : Valid a → Valid (.left a)
  | right : Valid a → Valid (.right a)
  | add : Valid a → Valid b → Disjoint a b → Valid (.add a b)
  | equiv : Equiv a b → Valid a → Valid b

def FreeRational := @Quot {x : Rat // Valid x} (Equiv ·.1 ·.1)

[Mario Carneiro]

This is including an axiom saying splits exist, i.e. $\forall x,\exists a b,a+b=x$

[Mario Carneiro]

but not specifically that half exists, which is why left and right are not the same

[Markus de Medeiros]

Mario Carneiro said:

what is add_left_cancel used for?

Only the CMRA.Cancellable instance right now, for which it seems necessary. No idea what else downstream.

[Shreyas Srinivas]

Mario Carneiro said:

sure, you can imagine the resources as a finite antichain in the complete binary tree, but then the "numbers" need to represent sets of leaves, not just one

Yes. But the sets would correspond to a subtree. So merging a set of resources would be collapsing a subtree to its root node.

[Mario Carneiro]

but there isn't necessarily one root node

[Shreyas Srinivas]

If some fragment of the subtree is actually moved, the corresponding subsubtree is transplanted to the other root node

[Shreyas Srinivas]

Mario Carneiro said:

but there isn't necessarily one root node

Root of a subtree.

[Shreyas Srinivas]

The overall tree has one root node that represents 1, and when the tree collapses to its root there is sole ownership again.

[Mario Carneiro]

if you have

    1
   / \
  d   c
 / \
a   b

then {b, c} can't be represented by the root node 1 because it's missing a

[Mario Carneiro]

there is no single node which represents {b, c}

[Mario Carneiro]

in the above inductive this would be add (right (left one)) (right one)

[Mario Carneiro]

and actually I don't think sets of nodes from the tree is enough, since if you decided to split {b, c} then there is no set of nodes that would be equivalent to (i.e. left (add (right (left one)) (right one)) isn't a set of nodes)

[Shreyas Srinivas]

If you split b and c, you would have a new internal node

[Mario Carneiro]

no, I'm splitting b + c

[Mario Carneiro]

not b or c

[Shreyas Srinivas]

Oh right

[Shreyas Srinivas]

But once we do b + c, do we care to keep their identities separate?

[Shreyas Srinivas]

Can’t they just be one thread carrying b and c as on big fragment of resource?

[Mario Carneiro]

we don't, but that's the problem, there is no single node representing that combination so now we can't draw children of that non-node to represent the result of splitting it

[Mario Carneiro]

we would need a representation where sums of elements are themselves elements

[Shreyas Srinivas]

In my idea you would combine the two nodes of b and c into one node

[Mario Carneiro]

which the inductive type does

[Mario Carneiro]

what does that mean?

[Shreyas Srinivas]

If it is the sole remaining child, then just delete and let the parent node represent the combination of b and c

[Mario Carneiro]

You can definitely do it if you have mutable state, the challenge here is that this "rational" type has to represent every possible split pattern and history

[Mario Carneiro]

if you have mutable state you just need a list of objects that add to 1

[Mario Carneiro]

and every split just removes that element and adds two more

[Shreyas Srinivas]

Let’s say you have a node structure a-> [b,c,d]. When merging b and c you create a combined node e. Then you get a -> [e,d]

[Shreyas Srinivas]

If you combine e and d into a new blob f, first that node becomes a -> [f]`

[Shreyas Srinivas]

Then because a has only one child

[Shreyas Srinivas]

a gets replaced by f

[Mario Carneiro]

but Rational is just a type, it isn't living in some particular context which keeps track of what other rationals have been created

[Mario Carneiro]

and in particular even if you did store that context inside each rational you would get in trouble when it goes out of date because you try to hold on to one piece while splitting another one

[Shreyas Srinivas]

My hope is that we don’t actually have to track exact numbers. After all we only care that we can merge the same things we split and check that we have all the pieces. Suppose we split a cake into pieces and put them in different plates on a table. We then put the pieces back on the cake tray. Even if we don’t rearrange them into the exact shape, and have a haphazard arrangement, ,we can determine that all the pieces we cut out have been returned. This is because all the plates are empty

[Shreyas Srinivas]

The tree analogy just introduces some bigger intermediate plates and the tree structure tracks which small plates derive their cake from which intermediate plate.

[Markus de Medeiros]

Iris is affine so you can lose plates

[Shreyas Srinivas]

Right, but even if someone steals a plate, we can track of whether someone owns a totality or part of the remaining cake by checking for emptiness of remaining plates

[Shreyas Srinivas]

Even in the rational number case, if some resource fragment just disappears, then thanks to our full ownership check (=?= 1) , the remainig fragments can’t sum up to 1.

[Shreyas Srinivas]

To be upfront, I can see the simplicity of just using rational numbers here. The more I think about this tree system, the more complicated it seems.

[Mario Carneiro]

Shreyas Srinivas said:

My hope is that we don’t actually have to track exact numbers. After all we only care that we can merge the same things we split and check that we have all the pieces. Suppose we split a cake into pieces and put them in different plates on a table. We then put the pieces back on the cake tray. Even if we don’t rearrange them into the exact shape, and have a haphazard arrangement, ,we can determine that all the pieces we cut out have been returned. This is because all the plates are empty

The free rational type is strictly harder than just tracking actual numbers. But really you don't need to do this in logical reasoning, you existentially quantify all of these numbers so you aren't actually working with them concretely anyway

[Mario Carneiro]

The point of this type is to have an abstract accounting mechanism that in principle does not forget anything

[Mario Carneiro]

that's what you need to prove the lemmas

[Mario Carneiro]

but in the program logic you don't actually need to deal with the numbers

[Markus de Medeiros]

Mario Carneiro said:

you existentially quantify all of these numbers

Well that's not strictly true, you could want a finitely splittable fractional resource for example (Nat+ with addition and One.one := n). But your overall point that program logics abstract over the concrete fractions is true.

[Mario Carneiro]

if you are doing finite splitting then yes you will have to do math

[Mario Carneiro]

maybe the fistful of dollars paper is doing that?

[Mario Carneiro]

(misremembered, that was not an iris paper, but https://iris-project.org/pdfs/2019-esop-time.pdf is the iris version)

[Markus de Medeiros]

IIRC that's different, more like the numbers CMRA's

[Mario Carneiro]

I guess if you want a finitely divisible read permission that would be something like a bounded concurrency primitive

[Markus de Medeiros]

Or maybe to specify an invariant for a size N circular buffer, something like [ exists n, Frac(n) * pure (sizeof buf + n = N) ]so if you have Frac i it is sound to add i elements to the buffer without overflow.

[Markus de Medeiros]

Anyways, this is interesting but no reason to add anything about splitting to Frac haha

[Mario Carneiro]

I don't see why you wouldn't just use numbers CMRA for that

[Markus de Medeiros]

Sure, yeah

[Mario Carneiro]

I think this discussion has been a bit too theoretical, we don't actually have the code that uses Frac

[Mario Carneiro]

the only motivation thus far is that it is one part of the stack to define something we want, but obviously that was added for a reason and I am sure we don't have anything that would notice if we just skipped that part

[Markus de Medeiros]

FYI: I did end up needing to add in class of fractions with splitting for this update lemma:

theorem dfrac_undiscard_update [IsSplitFraction F] :
    (.discard : DFrac F) ~~>: fun k => ∃ q, k = .own q