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

*From*: Akash <akash.gopkrish@xxxxxxxxx>*Date*: Fri, 8 Dec 2023 23:50:41 -0500*References*: <b167372b-d453-404c-a0c7-e4a2766c6a27n@googlegroups.com> <0926889F-DAF2-45F1-AEF6-A42B04734B24@gmail.com>

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?

On Fri, Dec 8, 2023, 1:01 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

A simple specification for the problem that you mention can be written as--TwoSum(S, tgt) ==LET GoodSum(x,y) == x + y = tgtIN { <<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).StephanOn 7 Dec 2023, at 19:52, Akash Gopalkrishnan <akash.gopkrish@xxxxxxxxx> wrote: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.

**Follow-Ups**:**Re: [tlaplus] How do you think abstractly***From:*Stephan Merz

**References**:**[tlaplus] How do you think abstractly***From:*Akash Gopalkrishnan

**Re: [tlaplus] How do you think abstractly***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] How do you think abstractly** - Next by Date:
**Re: [tlaplus] How do you think abstractly** - Previous by thread:
**Re: [tlaplus] How do you think abstractly** - Next by thread:
**Re: [tlaplus] How do you think abstractly** - Index(es):