search

Chymyst / chymyst-core

Declarative concurrency in Scala - The implementation of the chemical machine
Apache License 2.0
155 stars 11 forks source link

Comparison to Temporal Logic , FRP , TLA+ #160

Closed xekoukou closed 6 years ago

xekoukou commented 6 years ago

Is it possible to compare this to FRP and Temporal logic and provide some counterexamples on the expressiveness of FRP?

Another variant of temporal logic is TLA+ and it seems that one can model the philosophers' dinning problem : https://learntla.com/concurrency/processes/ (though this is written in plusCal)

I am interested in specifying self-organizing social systems and then creating the code that will enable their communication patterns. They are studied as Complex Systems and it seems that they draw many ideas from Statistical thermodynamics and Physics.

I haven't read this paper yet but it is one of the very few that uses formal methods (TLA+ , Event B) to prove properties about self-organizing systems. https://hal.archives-ouvertes.fr/hal-01726402/document

winitzki commented 6 years ago

@xekoukou I don't know TLA+ in great detail but I would think that FRP is strictly less expressive because it is limited to handling streams of data. FRP cannot express arbitrary synchronization between processes that are arbitrarily started and stopped, or start / stop each other. In particular, I think FRP cannot express the dining philosophers problem. This might be incorrect, I'm not an expert in formal specification. Let me know if you find something here!

xekoukou commented 6 years ago

I am not an expert in TLA+ either. Some characteristics of TLA+ is that : A. There is a global state that changes over time (a behavior). B. Some of the variables of the state do not need to express computations, they could describe the environment in which computation happens.

If I was to translate the chymyst model to TLA+ , the molecules would be the global TLA state and each reaction would be an action in TLA+. The 'always' G linear temporal operator is used in TLA+ to say that the (re)actions are always true. For every possible behavior, the next state must abide to the action rules.

Now, in Idris or Agda, proofs that take no part in computation are erased during compilation. I wonder if one could describe a distributed system and then erase all the imaginary vars that take no part in computation.