[ANN] interval-patterns-0.8.2

tonyday567:

The symbols attach to the numbers ⟦2 5⟧ is function application and hence a blank.

Interesting idea. Reminds me of bra-ket notation in physics. Perhaps we can interpret ⟦2 as an idempotent function, for example max 2. Likewise, 5⟧ would be min 5. The final convex set is then obtained by applying the chain of functions to Whole, just like what ShowS does.

The idea of describing points or sets by iterated functions is not new, of course. It is the basis of Conway’s surreal numbers and of signed-digit exact reals. There, the basic functions (digits) are certain contractions, represented as mid-pointing with a dyadic number.

By the way, Escardo and Simpson have a paper where they exhibit the closed real interval as the free mid-point algebra over two points. You might find that interesting. More general version here.