デカルト半環圏の基本的な自然同型

デカルト半環圏の構造と法則を与える同型射達。

/** 直積の結合律 */

command prod-assoc<A,B,C>


 [[A, B], C] -> [A, [B, C]] 
{

 [nth 1 | nth 1, [nth 1 | nth 2, nth 2]]

};
/** 直和の結合律 */

command sum-assoc<A,B,C>


 (@1 (@1 A | @2 B) | @2 C) -> (@1 A | @2 (@1 B | @2 C))
{

 when {

  1 => when { 1 => @1 pass, 2 => @2 @1 pass },

  2 => @2 @2 pass

 }

};
/** 直積の単位律 */

command prod-unit<A>


 [null, A] -> A
{

 nth 2

};
/** 直和の単位律 */

command sum-unit<A>


 (never | A) -> A
{

 pass

};
/* ゼロ法則 */

/* これはさすがに定義できない *

command zero<A>


 [never, A] -> never
{

};

*/
/** 直和の対称スワップ */

command sum-swap<A,B>


 (@1 A | @2 B) -> (@1 B | @2 A)
{

 when {1 => @2 pass, 2 => @1 pass}

};
/** 直和に対する直積の分配法則 */

command dist<A,B,C>


 [A, (@1 B | @2 C)] -> (@1 [A, B] | @2 [A, C])
{

 [nth 1 > x,  nth 2 > y];

 %y | when {1 => @1 [%x, pass], 2 => @2 [%x, pass]}

};