TLA+ minimum of function/sequence

[Thomas Gebert]

Hello!

I am currently trying to find the minimum value in a function; is there a relatively easy way to do this in TLA+?

Also, is there a way to get the N smallest values in a function?

[Stephan Merz]

Hello,

using the generic definitions

Range(f) == { f[x] : x \in DOMAIN f }

Min(S) == CHOOSE s \in S : \A t \in S : s <= t

you can write Min(Range(f)) to denote the minimum value that a function f takes, and TLC will be able to evaluate that expression as long as the domain of f is non-empty and finite. The generalization to find the N smallest values is left as an exercise to the reader. :-)

Evaluating the above definitions takes quadratic time in the domain of the function. If your function has a somewhat big domain and if both domain and co-domain are ordered, it may be worthwhile to sort the array (function) first.

Hope this helps,

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/076e423b-fe5b-4046-a9c4-bb7077e80f01%40googlegroups.com.

[Thomas Gebert]

In this case the function space is rather large; how would i go about doing a sort on a function?  The keys are in no particular order; is there a simple enough way to turn a function into a sequence of tuples (<<key,value>>)?

On Monday, December 23, 2019 at 6:22:53 AM UTC-5, Stephan Merz wrote:

Hello,

using the generic definitions

Range(f) == { f[x] : x \in DOMAIN f }

Min(S) == CHOOSE s \in S : \A t \in S : s <= t

you can write Min(Range(f)) to denote the minimum value that a function f takes, and TLC will be able to evaluate that expression as long as the domain of f is non-empty and finite. The generalization to find the N smallest values is left as an exercise to the reader. :-)

Evaluating the above definitions takes quadratic time in the domain of the function. If your function has a somewhat big domain and if both domain and co-domain are ordered, it may be worthwhile to sort the array (function) first.

Hope this helps,

Stephan

On 23 Dec 2019, at 06:24, Thomas Gebert <thomas...@gmail.com> wrote:

Hello!

I am currently trying to find the minimum value in a function; is there a relatively easy way to do this in TLA+?

Also, is there a way to get the N smallest values in a function?

--
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 tla...@googlegroups.com.

[Stephan Merz]

Below are definitions TLA+ operators that convert a set of integers into a sorted sequence. You can take the first N elements of SortedSeqFromSet(Range(f)) to retrieve the N smallest values of the function f. Evaluation of these operators still requires quadratic time, and although you could write a Quicksort operator in TLA+, if you really care about efficiency you should probably consider overriding the definition of SortedSeqFromSet(_) by a Java method.

Best,

Stephan

RECURSIVE InsertSorted(_,_,_), SortedSeqFromSet(_)

InsertSorted(x, seq, i) ==  \* insert element in a sorted sequence of integers, starting from index i

  IF i > Len(seq) THEN seq \o << x >>

  ELSE IF x <= seq[i] THEN SubSeq(seq, 1, i-1) \o << x >> \o SubSeq(seq, i, Len(seq))

  ELSE InsertSorted(x, seq, i+1)

SortedSeqFromSet(S) ==   \* convert a set of integers into a sorted sequence

  IF S = {} THEN << >>

  ELSE LET x == CHOOSE x \in S : TRUE

           rest == SortedSeqFromSet(S \ {x})

       IN  InsertSorted(x, rest, 1)

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/67e9079a-443d-4b28-a9f2-36ac7378d36f%40googlegroups.com.