tlaplus
Create Rationals module
This would enable division plus floor/ceiling functions, with the following benefits:
- Calculate the size of the majority of a set (currently passed in as a constant in the Paxos spec)
- Enable specification of algorithms requiring calculating midpoint of array (binary search, sorting, etc.)
Would theoretically include Java module override with an exact-representation Rationals implementation.
Related rescale operator and its TLC module override in https://gist.github.com/lemmy/1eaf4bec8910b25e206d070b0bc80754
A Rationals module that TLC can handle might be useful, but isn’t needed for the applications Andrew mentions. Programs generally implement them using only integer arithmetic with operators that are defined in the Integers module.
I wonder if implementing rationals is really any easier than implementing reals. Does the set of rationals being only countably infinite make it easier?
Leslie
From: Andrew Helwer [email protected] Sent: Monday, October 14, 2019 12:48 PM To: tlaplus/CommunityModules [email protected] Cc: Subscribed [email protected] Subject: [tlaplus/CommunityModules] Create Rationals module (#4)
This would enable division, with the following benefits:
- Calculate the size of the majority of a set (currently passed in as a constant in the Paxos set)
- Spec algorithms requiring calculating midpoint of array (binary search, sorting, etc.)
Would theoretically include Java module override with an exact-representation Rationals implementation.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ftlaplus%2FCommunityModules%2Fissues%2F4%3Femail_source%3Dnotifications%26email_token%3DAEUS3OSRBE2FSF3N2I3NRGDQOTEILA5CNFSM4JATJJC2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HRVZKTQ&data=02%7C01%7Clamport%40microsoft.com%7Cb13aeae7840a4bbf0b0808d750df77e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637066793032258515&sdata=Pm4vPGGuXbeO5DPLDpTzbvzJp0rlaeOQM12dDizDdYo%3D&reserved=0, or unsubscribehttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAEUS3OVP5T4WJTUBB6VRG2LQOTEILANCNFSM4JATJJCQ&data=02%7C01%7Clamport%40microsoft.com%7Cb13aeae7840a4bbf0b0808d750df77e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637066793032268522&sdata=XhnrJrYVgWgr2wXxmIoTwuUP8CqP4F84Vpu8xAS998Y%3D&reserved=0.
Adding integer division to the Integers standard module would work well, correct. Implementing rationals might be a better fit than implementing reals because things like equality checking actually work if you're using something like a pair <<int, uint>> (reduced with GCD after each operation) to represent it internally.
Integer division is already in the module—probably defined in the Naturals module that is imported by the Integers module. (It’s written \div.)
It is impossible to directly write an irrational number in TLA+. TLC would not be able to evaluate
CHOOSE x \in Real : x^2 = 2
But neither could it evaluate
CHOOSE x \in Rational : x^2 = ¼
Leslie
From: Andrew Helwer [email protected] Sent: Tuesday, October 15, 2019 6:40 AM To: tlaplus/CommunityModules [email protected] Cc: Leslie Lamport [email protected]; Comment [email protected] Subject: Re: [tlaplus/CommunityModules] Create Rationals module (#4)
Adding integer division to the Integers standard module would work well, correct. Implementing rationals might be a better fit than implementing reals because things like equality checking actually work if you're using something like a pair <<int, uint>> (reduced with GCD after each operation) to represent it internally.
Hmmm... it would be possible (although grossly inefficient) to implement CHOOSE x \in Rational : x^2 = 1/4 with the standard zig-zag enumeration of the Rationals, right? Although you can't easily restrict the rationals to a finite set like you can with the integers so this might be handing people a footgun. Or maybe TLC doesn't support lazy evaluation of infinite sets. Still, there are many ways to create unbounded monotonically-increasing behaviour with TLA+; why not add another!
Regardless, I think people do expect there are things you can write in TLA+ which work in TLC, and things you can't. I actually appreciate this approach over the "everything you can write can be model checked" strategy taken by other languages, which invariably restricts you from doing things the language designers never considered. Thus I personally would find it acceptable to only implement basic arithmetic & equality operators with the rationals.
But anyway this whole Rationals thing might be a solution in search of a problem, since the only applications I can think of are already solved by integer division. I'll keep a look out for places where I wished I had a rational type as I write more specs.
My point is not that TLC should not handle rationals. It’s that if it’s going to handle rationals, there’s no reason not to have it handle all reals. There are lots of applications for reals—in particular, real-time and hybrid algorithms. Currently, they can be handled only with discrete time measured in an integral number of clock ticks. That’s probably good enough, since it’s unlikely that a system has a bug that’s not discovered in a model with a clock measuring femtoseconds. But as far as I know, no one has ever tried.
From: Andrew Helwer [email protected] Sent: Tuesday, October 15, 2019 7:32 AM To: tlaplus/CommunityModules [email protected] Cc: Leslie Lamport [email protected]; Comment [email protected] Subject: Re: [tlaplus/CommunityModules] Create Rationals module (#4)
Hmmm... it would be possible (although grossly inefficient) to implement CHOOSE x \in Rational : x^2 = 1/4 with the standard zig-zag enumeration of the Rationals, right? Although you can't easily restrict the rationals to a finite set like you can with the integers so this might be handing people a footgun. Or maybe TLC doesn't support lazy evaluation of infinite sets. Still, there are many ways to create unbounded monotonically-increasing behaviour with TLA+; why not add another!
Regardless, I think people do expect there are things you can write in TLA+ which work in TLC, and things you can't. I actually appreciate this approach over the "everything you can write can be model checked" strategy taken by other languages, which invariably restricts you from doing things the language designers never considered. Thus I personally would find it acceptable to only implement basic arithmetic & equality operators with the rationals.
But anyway this whole Rationals thing might be a solution in search of a problem, since the only applications I can think of are already solved by integer division. I'll keep a look out for places where I wished I had a rational type as I write more specs.