programdemos/magmas.xtl
Magmas: a set with a binary operation that stays in the set, and nothing more is promised. Rock-paper-scissors is one: x played against y gives the winner (x on a tie). With its table we can ask which laws hold, for every case at once.
Run it with ./demos/magmas.xtl or "xetal run demos/magmas.xtl". It prints the Cayley tables of rock-paper-scissors and of its five-move extension, a 1 or 0 for each law checked, and draws the five-move table as an SVG file. Read the law checks: each is one comparison over a whole table, with no loop.
Rock-paper-scissors
ᵘr̲ps : Int -> Int -> Int
The winner of x played against y, moves numbered 1 rock, 2 paper, 3 scissors; on a tie, x.
ᵘr̲ps ← { x y → d ← (x − y) m̲od 3◆ y + (x − y) × d ≤ 1 }
names : Box Char
The move names, in the order of their numbers.
names ← "rock" "paper" "scissors"
t : Int
The Cayley table of u:r_ps: row x, column y holds x against y.
t ← (r̲ange 3) 'ᵘr̲ps t̲able r̲ange 3
Laws
ᵘc̲ommutative : (Match a, Truthy b) => (Int -> Int -> a) -> Int -> b
'f u:c_ommutative n: 1 when f, on 1 to n, gives the same table with its arguments swapped, else 0.
ᵘc̲ommutative ← { f̲ n → ((r̲ange n) 'f̲ t̲able r̲ange n) m̲atch (r̲ange n) '{ ⍵ f̲ ⍺ } t̲able r̲ange n }
ᵘi̲dempotent : Truthy a => (Int -> Int -> Int) -> Int -> a
'f u:i_dempotent n: 1 when x f x is x for every x in 1 to n, else 0.
ᵘi̲dempotent ← { f̲ n → (r̲ange n) m̲atch '{ ⍵ f̲ ⍵ } e̲ach r̲ange n }
ᵘa̲ssociative : Truthy a => (Int -> Int -> Int) -> Int -> a
'f u:a_ssociative n: 1 when (x f y) f z equals x f (y f z) for every triple from 1 to n, else 0.
ᵘa̲ssociative ← { f̲ n → t ← 1 + (3 r̲eshape n) e̲ncode o̲ffsets n ^ 3 x ← 1 s̲elect t y ← 2 s̲elect t z ← 3 s̲elect t '∧ r̲/ ((x f̲ y) f̲ z) = x f̲ y f̲ z }
ᵘi̲dentity : (Int -> Int -> Int) -> Int -> Int
'f u:i_dentity n: the element e of 1 to n with e f x and x f e both x for every x, or 0 when there is none.
ᵘi̲dentity ← { f̲ n → ⍝ the identity element, or 0 for none r ← r̲ange n e ← w̲here '{ (r m̲atch ⍵ f̲ r) ∧ r m̲atch r f̲ ⍵ } e̲ach r 0 = t̲ally e ? 0◆ f̲irst e }
Other magmas
ᵘa̲dd : Int -> Int -> Int
Addition modulo 3 on 1 2 3, where 1 stands for 0.
ᵘa̲dd ← { x y → 1 + (x + y − 2) m̲od 3 }
ᵘs̲ub : Int -> Int -> Int
Subtraction modulo 3 on 1 2 3, where 1 stands for 0.
ᵘs̲ub ← { x y → 1 + (x − y) m̲od 3 }
Rock-paper-scissors-lizard-Spock
ᵘr̲psls : Int -> Int -> Int
The winner of x played against y, moves numbered as in moves; on
a tie, x.
ᵘr̲psls ← { x y → d ← (x − y) m̲od 5◆ y + (x − y) × d ≤ 2 }
moves : Box Char
The five move names, in the order of their numbers.
moves ← "rock" "Spock" "paper" "lizard" "scissors"
w : Int
The Cayley table of u:r_psls.
w ← (r̲ange 5) 'ᵘr̲psls t̲able r̲ange 5