{-| Module : Docs.Additive Description : Examples and properties of the tile algebra Copyright : (c) David Janin, 2016 License : see the LICENSE file in the distribution Maintainer : janin@labri.fr Stability : experimental Sum, negation and few axioms from inverse semigroup theory. -} module Docs.Additive where import Tile.Tile -- * The additive monoid of tiles -- -- ** temporal values -- | A basic atomic tile (temporal value): -- -- @ -- b0 = fromDurationAndValueT 3 'a' -- @ -- -- It can be depicted by -- -- <<ex1.svg A basic temporal value>> -- -- with duration d=3 and value v='a'. b0 :: Tile Integer Char Char b0 = fromDurationAndValueT 3 'a' -- ** Delay -- | A basic delay tile: -- -- @ -- b1 = fromDurationT 3 -- @ -- -- It can be depicted by -- -- <<ex2.svg A delay>> -- -- with duration d=3. Forgeting values is handled by the /delayT/ functions with -- -- prop> b1 == delayT b0 b1 :: Tile Integer Char Char b1 = fromDurationT 3 -- ** Sum -- | The sum of two tiles amounts to merge the output root of the first one with the inoput root of the second. -- -- @ -- b2 = x + y -- @ -- -- It can be depicted by -- -- <<ex3.svg A simple sum>> -- -- with x = fromDurationAndValueT 3 'a' and y = fromDurationAndValueT 2 'b'. -- -- Property: function delayT is functorial over sum: -- -- prop> delayT (x+y) == delayT x + delayT y b2 :: Tile Integer Char Char b2 = fromDurationAndValueT 3 'a' + fromDurationAndValueT 2 'b' -- ** Negation -- | The negation of a tile amounts to flip input and ouput roots. -- -- @ -- b3 = -x -- @ -- -- It can be depicted by -- -- <<ex4.svg A negated tile>> -- -- with x = fromDurationAndValueT 3 'a'. -- -- Property: the negation distributes over sums reversing it. -- -- prop> - (x+y) == - y - x b3 :: Tile Integer Char Char b3 = - fromDurationAndValueT 3 'a' -- ** Difference -- | The induced difference x - y defined as x + (-y). -- -- @ -- b4 = x - y -- @ -- -- It can be depicted by -- -- <<ex5.svg A tile difference>> -- -- Property : delayT is also functorial with respect to difference -- -- prop> delayT (x - y) == delayT x - delayT y b4 :: Tile Integer Char Char b4 = fromDurationAndValueT 3 'a' - fromDurationAndValueT 2 'b' -- ** Spatio-temporal resulting zigzags -- | Temporal zigzag as a more general structure -- -- @ -- b5 = x1 - x2 + x3 -x4 -- @ -- -- It can be depicted by -- -- <<ex6.svg A zigzag>> -- -- with x1 = fromDurationAndValueT 3 'a', x2 = fromDurationAndValueT 5 'b', -- x3 = fromDurationAndValueT 7 'c' and x4 = fromDurationAndValueT 3 'd' b5 :: Tile Integer Char Char b5 = fromDurationAndValueT 3 'a' - fromDurationAndValueT 5 'b' + fromDurationAndValueT 7 'c' - fromDurationAndValueT 3 'd' -- ** Semigroup inverse -- | Merging parallel temporal values -- -- @ -- b6 = x - x + x -- @ -- -- Both x and x - x + x are depicted by -- -- <<ex7.svg A negated tile>> -- -- and we have -- -- prop> x == x - x + x b6 :: Tile Integer Char Char b6 = fromDurationAndValueT 3 'a' - fromDurationAndValueT 3 'a' + fromDurationAndValueT 3 'a' -- ** Idempotent tiles -- | The coreset co[x] of a tile x is obtained by moving its input root to its ouput root. Dually, -- the reset re[y] of a tile is otained by moving its ouput root to its input root. -- -- -- @ -- b7 = co[x] + re[y] -- @ -- -- When input and out roots coincides, as in co[x] or re[y], elements are idempotents. -- -- <<ex8.svg A gneric idempotent>> -- -- and we have: -- -- prop> re[x] == x - x and x == re[x] + x -- prop> co[y] == -y + y and y == y + co[y] b7 :: Tile Integer Char Char b7 = co [fromDurationAndValueT 3 'a'] + re[fromDurationAndValueT 2 'b']