[tlaplus] Re: Defining a function in terms of variables in TLA

[marta zhango <martazhango@xxxxxxxxx>]

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.

On Thursday, November 21, 2024 at 3:31:02 PM UTC+12 Andrew Helwer wrote:

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

On Wednesday, November 20, 2024 at 5:28:20 AM UTC-5 marta zhango wrote:

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 ?

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/cdf5de0d-7720-4c28-b5e6-7d1f8323ef98n%40googlegroups.com.