Example of LTL with functional programming in JS

Creating a new query language specialized in event processing
profile photo
Julien Vinckel

LTL

Take two very complex subjects, LTL and functional programing, mix them...
And you get Potions Events Query
Reading Eric Elliott blog on Composing Software, I realized that LTL is all about composing predicates. I found a way to apply what I've just learnt
We start with an alphabet, a set of Atomic Propositions AP = {p1, p2}
A Property is a set of infinite Words over the alphabet, the power set of AP.
(Optional in our case) A Transition System satisfies the property P if the Traces of the Transition System are contained in P
There are different ways of specifying a Property : finite automata, w-regular expression and a combination of (G, F, X, GF) called linear temporal logic LTL.
The combinations of G, F, X and GF are called Formulas.
Here is the syntax of a Formula
  • the "true" formula is satisfied by any word / execution
  • any Atomic Proposition of AP is an LTL formula and is satisfied if the first letter of the word contains the atomic proposition
  • LTL formula Phi1 AND LTL formula Phi2 if Phi1 AND Phi2 are satisfied
  • NOT LTL formula Phi1 is satified if Phi1 is not satisfied
  • X LTL formula Phi1 is satisfied if thee next letter satisfies Phi1
  • Phi1 UNTIL Phi2 is satisfied if Phi2 is satisfied and till then Phi1 is satisfied.
  • Implicatio
    • Image without caption
Image without caption
For finite LTL formula (called LTLf) we can use the following operators
file:///Users/julienvinckel/Downloads/Factures%202021_10_01/12250-55566-1-PB.pdf
Image without caption
We can find composite operator, and the one that is interesting to us : precedence
www.cds.caltech.edu
Image without caption

Potions LTL in javascript (Functional programing)

chalk-talk/LTL at main · PotionsCook/chalk-talk
Very small javascript programs to learn and eventually teach some coding principles - chalk-talk/LTL at main · PotionsCook/chalk-talk
chalk-talk/LTL at main · PotionsCook/chalk-talk
LTL provides a library to ease the composition of LTL formulas in javascript.
For instance it enables in a few lines of code to test
  • if a word satisfies : has an 'r' eventually followed by an 'e'
    • javascript
      import {f_ap, after} from "./ltl.js" // An atomic proposition factory const ap = letter => f_ap(value => letter === value); // The predicate has an "e" after an "r" const predicate = after(ap("r"))(ap("e")) console.log(predicate([...'superb'])) // returns false console.log(predicate([...'superbe'])) // returns true
  • the same way, if a sequence of events satisfies: has an event 'saw_product' eventually followed by a 'purchase'
    • javascript
      import {f_ap, after} from "./ltl.js" // seque const sequence_1 = [{name:'saw_product'}, {name:'purchase'}] const sequence_2 = [{name:'saw_product'}] // An atomic proposition factory const ap = event_name => f_ap(event => event_name === event.name); // The predicate has an "e" after an "r" const predicate = after(ap("saw_product"))(ap("purchase")) console.log(predicate(sequence_2)) // returns false console.log(predicate(sequence_1)) // returns true
But also way more complex predicates like the one described in Google Analytics Segments.
Segments - Feature Reference | Analytics Core Reporting API | Google Developers
This document provides an overview of segments in Google Analytics. There is an updated version of the Google Analytics Reporting API. We recommend migrating your code today to take advantage of the new API's key features. Segments allow you to select users and sessions to answer questions that are important to your business.
Segments - Feature Reference | Analytics Core Reporting API | Google Developers

Why ?


I recently read in full Eric Eliott amazing Medium pages on composing software. I advised all software developers interested in functional programming to do the same.
By the end of your read you'll be confident in saying :
“A monad is just a monoid in the category of endofunctors. What’s the problem?”
Composing Software: The Book
"Composing Software", the hit blog post series on functional programming and software composition in JavaScript is now a best selling book on Leanpub. Also available in print. On February 18th, 2017...
Composing Software: The Book
I've also been looking into simple ways to query sequences of events in the browser.
For instance querying a user who did A then B is not an easy task with simple SQL queries.
This is how I came across Linear Temporal Logic which appears to me extremely understudied in regular software development and "could be"/"is" an amazing tool to check if a software is functioning correctly.
This video might help you understand the key concepts of the LTL grammar
Related posts
post image
Functional programming
Start thinking declaratively
Why move from imperative to declarative code
post image
Summing up Eric Eliott composing software
post image
The actor model - trick to never complete the channel
Powered by Notaku