[Agda] LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs

[Alan Jeffrey]

On 11/15/2011 03:39 PM, Peter Hancock wrote:
> On 10/11/2011 15:17, Alan Jeffrey wrote:
>
>> LTL Types FRP: Linear-time Temporal Logic Propositions as Types,
>
> This seems very interesting.  I've looked a bit through it.

Thank you!

> Do you have any sense of what would happen if you dropped the "O" (next state)
> modality from LTL? Would that be a disaster?

Just dropping next doesn't lose much in terms of expressivity, the main 
place it's used is in the definition of decouple. Almost always, 
decouple is used when A is a Set (rather than an RSet) so you can 
recover the common case, as:

   decouple+ : Delay+ -> [[ <A> \rhd <A> ]]

where Delay+ is a type of non-zero delays.

Moving from discrete time to continuous time is more problematic, see 
the discussion of Zeno processes at the end of the paper. (The notion of 
Zeno process goes back at least the the late 80s / early 90s work on 
timed process algebra, although I'm not entirely sure who to credit; 
obviously Zeno's paradox itself is a teeny tiny bit older :-)

> There are fragments of LTL which are "invariant under stuttering": Lamport is
> very insistent on the importance of this notion.
> http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html
> Have you encountered anything bearing on this?

The behavioural model of FRP is essentially free of stuttering, since 
the model of A behaviours is (Time -> A). In particular there's a "hold" 
function that takes a series of A events and produces an A behaviour. 
The hold function masks stuttering: if the same event occurs on the 
input stream, it is undetectable on the output stream. So as long as 
you're programming using behaviours rather than events, you're invariant 
under stuttering.

A.

>
> Hank
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda