RE: [tlaplus] Re: Type checking and custom infinite sets

I would be surprised if you could not write your definition in TLA+ using the CHOOSE operator and recursively defined operators. I expect that recursive operator definitions are not described in the summary of TLA+ I pointed you to because that summary was taken from “Specifying Systems”, and they were added to the language after that book was written. (I should update it.) They’re described here:

https://lamport.azurewebsites.net/tla/tla2.html

From: Chris Jensen <cjjensen01@xxxxxxx>
Sent: Monday, November 8, 2021 2:10 AM
To: tlaplus@xxxxxxxxxxxxxxxx; Leslie Lamport <tlaplus.ll@xxxxxxxxx>
Subject: Re: [tlaplus] Re: Type checking and custom infinite sets

You don't often get email from cjjensen01@xxxxxxx. Learn why this is important

Hi!

Thanks for the reply. The specific set I want to define is inductively defined/constructed, with the predicate being equivalent to a proof that the element is possible to construct (in a prolog style fashion).

From the linked summary, it doesn't seem that this is possible, however I read somewhere that it was possible to overload values to use a Java module (see Nat). Is there any documentation on how to do this?

In the short term I'm planning on generating a sufficiently large finite subset and hoping that values outside of it are not generated.

Thanks,

Chris

On Saturday 06 November 2021 11:27:02 AM (+00:00), Leslie Lamport wrote:

A predicate does not define a set. The TLA+ operators for constructing sets are listed under the "Sets" heading on the "Constant Operators" section of:

https://lamport.azurewebsites.net/tla/summary-standalone.pdf

If the "set" you want to define cannot be expressed with them, it is probably not what mathematicians define to be a set.

Leslie

On Friday, November 5, 2021 at 11:05:58 AM UTC-7 Chris Jensen wrote:

Hi!
When you have a type invariant for a system like Paxos, you can check that
for example ballot numbers are members of the set of natural numbers.

What I am trying to do (and can't seem to find any documentation on) is how
to define my own infinite sets (for example one which is defined by some
predicate).
This is specifically just for type checking, and thus should just be
checking whether a value is an element of a set, hence should just be able
to use the predicate.

Is there any way to do this?

--
Thanks,

Chris

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3ad9a5c4-d76f-4e8b-b670-e2378ee46155n%40googlegroups.com.

--
Thanks,

Chris