Re: [tlaplus] Polynomials in PlusCal?

[Stephan Merz <Stepha...@xxxxxxxxx>]

Hello John,

welcome to the TLA+ group.

Your project sounds interesting. However, first it is not clear to me that what you are proposing is restricted to PlusCal in any way. Remember that PlusCal is getting translated to TLA+ and that the ordinary TLA+ tools (TLC and the prover) are used on the result of the translation. 

Second, what would your back-end for comparing these expressions actually be? The existing tools will not natively support the symbolic computations that you are interested in, although you can use them for testing assertions on fixed values, as you say.

If you are focusing on symbolic comparisons of polynomials, using a dedicated solver such as Redlog (http://www.redlog.eu) may be the easier path – assuming you do not get any benefit from the TLA+ / PlusCal environment.

Best,
Stephan


On 12 Sep 2014, at 18:34, jwb...@xxxxxxxxx wrote:

> Hi everyone,
> 
> I would like to compare, symbolically, some mathematical expressions that get built up in a numerical application I am specifying in PlusCal.  My first thought is to write a module for multivariate polynomials and use it in place of PlusCal's built-in arithmetic operations.  I would then make intermittent assertions about polynomials and check them for functional correctness with TLC.
> 
> For my application, I believe this "symbolic" approach is a better fit than a discrete sampling from real numbers.
> 
> If anyone has thoughts or suggestions, however, I would be much obliged.
> 
> Thanks,
> John
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.