Defining a function in terms of variables in TLA

[marta zhango]

How can I define a function of time or some other variable, say of a seismogram

in TLA ?  But without specifying the mapping.

Using a VARIABLE, LET, or something else ?

[Hillel Wayne]

Could you provide a pseudocode example of what you're looking for, and some information on what you've already tried?

H

--
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 visit https://groups.google.com/d/msgid/tlaplus/fe0b118c-2efd-4519-8e43-0f8587d697b2n%40googlegroups.com.

[Andrew Helwer]

If you're using this for writing proofs over it, you'll probably make the function a constant then define some set of assumptions over it. Like:

CONSTANT f

ASSUME f \in [Real -> Real]

ASSUME IsContinuous(f) /\ IsDifferentiable(f)

Where you define IsContinuous and IsDifferentiable to mean some definition you can use in proofs. However, if you want to formally verify the proofs then TLAPM does not really support reasoning over Reals at this time. Some researchers developed an extension for it which you can read about here, but this work has not yet been integrated into the main development branch.

Andrew Helwer

[marta zhango]

Right.  TLA+ and TLAPM is not used here because the requirements of handling industrial

applications require it to be a little more complicated.

I want to use formulas and decomposing them into smaller pieces. This is done using simple

definitions, rather than the more complex constructs of coding languages.  To formalize mathematics

and make it easier to write a proof.

This was discussed in "How to Write a Proof" by  Leslie Lamport in 1993.

Are there also other possibilities, using a variable for instance?  How would one define the time

variable?

The seismogram f(t) is a stachastic generated function of time, not necessarily correlated

with an earthquake, but a more general recording of incessant earth motion.

[marta zhango]

I would use the <1> <2> nomenclature, and will do a mathematical proof as in a book,

not as a program check of the proof.  In a way that would make it easier to check the proof

and construct the TLAPS code in future.   I am currently have to deal with constructs that might

not be defined at this time.

Would like to see how much progress I can do in providing mathematical proof sketches.

This is my main intention.

[marta zhango]

I currently want to define the Fourier Transform on a stochastic generated seismogram h(t).

That is, define the fourier mapping upon h(t).

Thus F(h(t)) = Integral h(t) exp^{-iwt} dt

And then show the proof of the linearity of the Fourier Transform

Thus

h(t) = a f(t) + b g(t) 

F(h(t)) = a F(f(t)) + b F(g(t))