How do you think abstractly

[Akash Gopalkrishnan]

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!

[Chris Ortiz]

Hi Akash, for TLA+ I think instead of set of integers you would like to give it as sequence of integers since sequence has a DOMAIN of unique integer indexes starting from 1 (which is actually the position of the elements in the sequence). But with sequences you can have repeat of the same integer and can change ordering as well which can give you different pairs. 

Like you, I am learning TLA+. I found TLA+ for me both for writing algorithms and specifying algorithm. It sometimes help me learn my algorithm better by creating it in TLA+. I hope this helps. Thanks.

[Stephan Merz]

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

--
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/b167372b-d453-404c-a0c7-e4a2766c6a27n%40googlegroups.com.

[Akash]

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?

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0926889F-DAF2-45F1-AEF6-A42B04734B24%40gmail.com.

[Stephan Merz]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFZmCwChio673OGeZFz5N3u4U02cHTK6FAiy2MjED83iDeJAFA%40mail.gmail.com.