| I'd use similar predicates to specify the intended result. For example, one way to specify the merge of two sorted integer sequences is as follows:
Range(f) == {f[x] : x \in DOMAIN f} \* better: extend CommunityModules Monotonic(f) == \A x,y \in DOMAIN f : x \leq y => f[x] \leq f[y]
Merge(s,t) == CHOOSE u \in Seq(Int) : /\ Len(u) = Len(s) + Len(t) /\ \E f \in [1 .. Len(s) -> 1 .. Len(u)], g \in [1 .. Len(t) -> 1 .. Len(u)] : /\ Monotonic(f) /\ Monotonic(g) /\ Range(f) \inter Range(g) = {} /\ Range(f) \union Range(g) = 1 .. Len(u) /\ \A i \in 1 .. Len(s) : u[f[i]] = s[i] /\ \A i \in 1 .. Len(t) : u[g[i]] = t[i]
Note that if you'd like to evaluate this operator using TLC, you'll have to rewrite the CHOOSE so that the quantifier ranges over a finite set, for example
CHOOSE u \in [1 .. Len(s) + Len(t) -> Range(s) \union Range(t)]
Again, such operators just serve as a logical specification of the result, they do not describe an algorithm for computing it.
Stephan On 9 Dec 2023, at 05:50, Akash <akash.gopkrish@xxxxxxxxx> wrote:
I think I understand your answer. You have put it abstractly but in algorithm form like Leslie did for quicksort. As a follow up, how would you specify the classic merge 2 sorted arrays problem or something like 0/1 knapsack? A simple specification for the problem that you mention can be written as
TwoSum(S, tgt) == LET GoodSum(x,y) == x + y = tgt IN { <<x, y>> \in S \X S : GoodSum(x,y) }
This operator will return all pairs of values in S whose sum equals tgt. (Note that it doesn't make sense to talk of an index of a number in a set, since sets are by definition unordered. Also, you may want to exclude symmetric solutions by requiring x <= y as part of the definition GoodSum. It is an easy exercise to adapt the definition to the case where S is a sequence of numbers and the result is the set of pairs of indexes.)
I presume that you would probably not consider the definition above to be an "algorithm" because it doesn't tell you how to compute the result effectively, let alone efficiently. You can use TLA+ to specify an algorithm that computes the set step by step, then assert that when the algorithm terminates given as input a set of integers S and an integer value tgt, its result agrees with TwoSum(S, tgt).
Stephan
I'm trying to learn TLA+ to solve Leetcode problems?
Is TLA+ for writing algorithms or just specifying algorithms. In other words, do i learn the algorithm first, or can I use TLA+ to create an algorithm?
For example, for the classic 2 sums problem: Given a set of integers. and a target value. Find the index of every pair of numbers that sum to the target value. Note: the index cannot be the same in the pair.
Thanks so much for the help!
--
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/b167372b-d453-404c-a0c7-e4a2766c6a27n%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/0926889F-DAF2-45F1-AEF6-A42B04734B24%40gmail.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/CAFZmCwChio673OGeZFz5N3u4U02cHTK6FAiy2MjED83iDeJAFA%40mail.gmail.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/620FA81C-54B4-427F-AE8A-8E11F51A4F6C%40gmail.com.
|