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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 15 Sep 2014 05:20:22 -0700 (PDT)*References*: <0a651653-cd9b-4fbf-8bcb-8502736a5fc5@googlegroups.com>

Hi John,

Stephan is traveling and won't be able to respond soon, so I'll try to

answer your question. First of all, you write

How does one say what it means for (certain types of)

numerical programs to be correct?

TLA+ allows you to express mathematics precisely. It doesn't tell you

how to figure out what mathematics you want to express. You write

A simple declarative statement (like Ax = b) at the termination

of an iterative algorithm would be easy to state but impossible

to prove

I presume here A is an array and x and b are vectors, all of reals,

and the problem is that this equality is not going to be ensured by an

algorithm because either (1) it does finite precision arithmetic or

(2) even though it's doing arithmetic with reals, it will not converge

to the correct result in a finite number of iterations. In either

case, you probably want to verify something like |Ax - b| < epsilon

for some suitable epsilon. Numerical analysts have done a lot of work

on this problem--work that I know nothing about. On the other hand,

you spoke about symbolic computation, so maybe you have something else

in mind.

In any case, we'll need to have a better idea of what you want to do

before we can help you. I suggest that we take this off the group

and you reply just to Stephan and/or me.

Leslie

**References**:**Polynomials in PlusCal?***From:*jwb . . .

- Prev by Date:
**Re: [tlaplus] Polynomials in PlusCal?** - Next by Date:
**2 Phase Commit in PlusCal** - Previous by thread:
**Re: [tlaplus] Polynomials in PlusCal?** - Next by thread:
**2 Phase Commit in PlusCal** - Index(es):