[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ minimum of function/sequence



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)


On 23 Dec 2019, at 22:02, Thomas Gebert <thomasgebert@xxxxxxxxx> wrote:

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


-- 
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/67e9079a-443d-4b28-a9f2-36ac7378d36f%40googlegroups.com.

--
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/826397D5-5C3D-42AF-A560-B019523B5411%40gmail.com.