OKlibrary  0.2.1.6
LiteralStructures.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.8.2010 (Swansea) */
00002 /* Copyright 2010, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 
00025 
00026 /* ******************************
00027    * Boolean literal structures *
00028    ******************************
00029 */
00030 
00031 /*
00032   A "boolean literal structure" is a pair [L,inv], where L is a set (the set
00033   of "literals") and inv a self-inverse bijection of L (the involution or
00034   "complementation").
00035 
00036   Abbreviation: "blitstr".
00037 
00038   Morphisms f: [L,inv] -> [L',inv'] are maps f: L -> L' such that
00039   f(inv(x)) = inv'(f(x)) for all x in L.
00040 */
00041 
00042 /* Checking whether L is a blitstr: */
00043 blitstr_p(L) := 
00044   listp(L) and is(length(L)=2) and 
00045   setp(first(L)) and
00046   is(map(second(L),first(L)) = first(L)) and
00047   every_s(lambda([x], is(second(L)(second(L)(x)) = x)), first(L))$
00048 
00049 /* Checking whether the blitstr L has a self-complementary literal: */
00050 has_scl_blitstr_p(L) := some_s(lambda([x], is(second(L)(x) = x)), first(L))$
00051 
00052 
00053 /* *********************
00054    * Checking equality *
00055    *********************
00056 */
00057 
00058 /* Checking whether the blitstr's L1 and L2 are equal: */
00059 blitstr_equalp(L1,L2) :=
00060   is(first(L1) = first(L2)) and
00061   every_s(lambda([x], is(second(L1)(x) = second(L2)(x))), first(L1))$
00062 
00063 
00064 /* *************
00065    * Morphisms *
00066    *************
00067 */
00068 
00069 /* Checking whether f is a blitstr-morphism from L1 to L2: */
00070 morphism_blitstr_p(f,L1,L2) :=
00071   every_s(lambda([x], elementp(f(x), first(L2)) and
00072             is(f(second(L1)(x)) = second(L2)(f(x)))),
00073           first(L1))$
00074 
00075 
00076 /* *****************
00077    * Constructions *
00078    *****************
00079 */
00080 
00081 /* The (unique) initial object (the empty blitstr): */
00082 initial_blitstr : [{},identity]$
00083 
00084 /* The terminal object, using the (self-complementary) literal []: */
00085 terminal_blitstr : [{[]},identity]$
00086 
00087 /* The boolean blitstr, with two literal 0, 1: */
00088 bool_blitstr : [{0,1},lambda([x],1-x)]$
00089 
00090 /* The free blitstr over the set X, with literal-set X x {0,1}: */
00091 free_blitstr(X) := [cartesian_product(X,{0,1}), lambda([x], [first(x),1-second(x)])]$
00092 
00093 /* The cofree blitstr over the set X, with literal-set X x X: */
00094 cofree_blitstr(X) := [cartesian_product(X,X), lambda([x], reverse(x))]$
00095 
00096 /* The product-blitstr of the list LL of blitstr's: */
00097 product_blitstr(LL) := 
00098   [uaapply(cartesian_product,map('first,LL)),
00099    buildq([I : map('second,LL)], lambda([x], map('apply, I, map("[",x))))]$
00100 /* The projections belonging to component i: */
00101 projection_product_blitstr(i) :=
00102   buildq([i],lambda([x],x[i]))$
00103 
00104 /* The coproduct-blitstr of the list LL of blitstr's: */
00105 coproduct_blitstr(LL) :=
00106   [set_sum(map(first,LL)),
00107    buildq([I : map('second,LL)], lambda([x], [I[second(x)](first(x)), second(x)]))]$
00108 /* The injections belonging to component i: */
00109 injection_coproduct_blitstr(i) :=
00110   buildq([i],lambda([x],[x,i]))$
00111 
00112 
00113 /* ****************
00114    * Translations *
00115    ****************
00116 */
00117 
00118 /* Converting a set of boolean literals into a blitstr (if 0 is in L,
00119    then we obtain the self-complementary literal 0):
00120 */
00121 sl2blitstr(L) := [union(L,map("-",L)), lambda([x],-x)]$
00122