On Sun, Feb 09, 2025 at 09:03:57PM +0100, Waldek Hebisch wrote:
>
> > So feel free to do whatever you want with IsArrow?
>
> Well, from the above you can see that I would write rather different
> categories and domains that you did. But I do not want to break
> what works, so I will probably do only minimal changes.
Attached is my proposed diff to logic.spad. I removed 'setVert'
and 'setArr': setting things separately may easily break properties
of a poset, so it is probably better not to have them. Removed
'completeReflexivity', 'completeTransitivity' and 'isAntisymmetric?':
poset is supposet to be reflexive and transitive, so those
should be no-ops for posets. Poset is supposed to be antisymmetric,
so 'isAntisymmetric?' should always return true, and conseqently
'isAntisymmetric?' does not give any new information.
I added internal function to compute transitive closure and called
it from 'addArrow!' so that we always get a poset. I also added
internal function for checking antisymmetry, so 'addArrow!' can
check if we still have a poset (and signal error otherwise).
Also, added internal functions for convertion between list of list
of booleans and boolean matrices: operations on matrices are
easier and more efficient.
Ater changes the following gives sensible result:
i1 := initial()$FinitePoset(Integer)
g1 := addObject!(i1, 1)$FinitePoset(Integer)
i1
g2 := addObject!(g1, 2)$FinitePoset(Integer)
t2 := addArrow!(g2, 1, 2)
g3 := addObject!(t2, 3)$FinitePoset(Integer)
addArrow!(g3, 2, 3)
addArrow!(g3, 1, 3)
Trying the same with current trunk shows that i1 is modified,
(so despite docstring 'addObject!' were modifying i1),
also operations in trunk leads to non posets.
Also I removed bunch of duplicate implementations.
Possible changes that I did not do:
- changing declaration of addArrow! so that it takes elements of
S instead of integer indices
- several functions (like kgraph) are really not applicable to posets,
optimaly their declaration should be removed, worse possiblity but
still better than current one is to signal errors on any attempt
to use them
- AFAICS bunch of functions makes sense for posets, but has fake
implementations which return different thing than promised
- non-mutating functions would be normally called 'addObject'
and 'addArrow' (that is without exclamation sign).
Also, most of things declared in FiniteGraph are given fake implementation,
as I wrote, it would be better avoid declaring FiniteGraph in Poset,
but intead, declare FiniteGraph in places when you can really
implement it.
One more thing: ATM there is bunch of internal functions, some
are potentially reusable. If reuse is desirable we could move
reusable functions to a separate package and use to either from
Poset or from FinitePoset.
In slightly different spirit: there are resonably natural functions
that Poset does not declare.
--
Waldek Hebisch
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to fricas-devel+unsubscr...@googlegroups.com.
To view this discussion visit
https://groups.google.com/d/msgid/fricas-devel/Z6lRW9UnFTipu7at%40fricas.org.
diff --git a/src/algebra/logic.spad b/src/algebra/logic.spad
index 02c36cc8..f4cbe066 100644
--- a/src/algebra/logic.spad
+++ b/src/algebra/logic.spad
@@ -659,12 +659,6 @@ Poset(S) : Category == Definition where
++ Note: different from getArrows(s) which is inherited from
++ FiniteGraph(S)
- setVert : (s : %, v : List S) -> Void
- ++ setVert(s, lv) sets the list of all vertices (or objects)
-
- setArr : (s : %, v : List List Boolean) -> Void
- ++ setArr(s, la) sets the list of all arrows (or edges)
-
addObject! : (s : %, n : S) -> %
++ addObject!(s, n) adds object with coordinates n to the
++ graph s.
@@ -735,20 +729,6 @@ Poset(S) : Category == Definition where
objectToIndex : (s : %, obj : S) -> NNI
++ objectToIndex returns the index of a given object.
- completeReflexivity : (s : %) -> %
- ++ Reflexivity requires forall(x): x<=x
- ++ This function enforces this by making sure that every element has
- ++ arrow to itself. That is, the leading diagonal is true.
-
- completeTransitivity : (s : %) -> %
- ++ Transitivity requires forall(x, y, z): x<=y and y<=z implies x<=z
- ++ This function enforces this by making sure that the composition
- ++ of any two arrows is also an arrow.
-
- isAntisymmetric? : (s : %) -> Boolean
- ++ Antisymmetric requires forall(x, y): x<=y and y<=x iff x=y
- ++ Returns true if this is the case for every element.
-
isChain? : (s : %) -> Boolean
++ isChain?(s) checks if s is a chain, that is any two elements
++ in s are comparable.
@@ -786,80 +766,69 @@ Poset(S) : Category == Definition where
dim : NNI := #(getVert(s)) + 1
obs : List S := concat(getVert(s), n)
arrows := []$List(List(Boolean))
- for a in getArr(s) repeat
- width : NNI := #a
- padding : Union(NNI, "failed") := subtractIfCan(dim, width)
- if padding ~= "failed" then
- diff : NNI := padding::NNI
- --print(("addObject diff=", string(diff))$String)])
- for x in 1..diff repeat
- a := concat(a, false)
- if empty?(arrows)
- then arrows := [a]
- else arrows := concat(arrows, a)
- emptyRow : List Boolean := [false for x in 1..dim]
- arrows := concat(arrows, emptyRow)
- finitePoset(obs, arrows)
-
- -- TODO - make this non-mutable
+ for row in getArr(s) repeat
+ row2 := concat(row, false)
+ arrows := cons(row2, arrows)
+ emptyRow : List Boolean := [i = dim for i in 1..dim]
+ arrows := cons(emptyRow, arrows)
+ finitePoset(obs, reverse!(arrows))
+
+ bll_to_mat(dim : NNI, arr : List(List(Boolean))
+ ) : TwoDimensionalArray(Boolean) ==
+ mat := new(dim, dim, false)$TwoDimensionalArray(Boolean)
+ for row in arr for i in 1..dim repeat
+ for y in row for j in 1..dim repeat
+ mat(i, j) := y
+ mat
+
+ mat_to_bll(mat : TwoDimensionalArray(Boolean)
+ ) : List(List(Boolean)) ==
+ dim : NNI := nrows(mat)
+ arr : List(List(Boolean)) := []
+ for i in dim..1 by -1 repeat
+ row : List Boolean := []
+ for j in 1..dim repeat
+ row := cons(mat(i, j), row)
+ arr := cons(reverse!(row), arr)
+ arr
+
+ transitive_closure!(mat : TwoDimensionalArray(Boolean)) : Void ==
+ dim : NNI := nrows(mat)
+ for j in 1..dim repeat
+ for i in 1..dim repeat
+ if mat(i, j) then
+ for k in 1..dim repeat
+ mat(i, k) := mat(i, k) or mat(j, k)
+
+ anitsymmetric?(mat : TwoDimensionalArray(Boolean)) : Boolean ==
+ dim : NNI := nrows(mat)
+ for i in 1..dim repeat
+ for j in 1..dim repeat
+ i = j => iterate
+ if mat(i, j) and mat(j, i) then return false
+ true
+
-- adds an arrow to this graph, where:
-- s is the graph where the arrow is to be added
-- n1 is the index of the start object
-- n2 is the index of the end object
addArrow!(s : %, n1 : NNI, n2 : NNI) : % ==
- a : List Boolean := qelt(getArr(s), n1)
- setelt!(a, n2, true)
- setelt!(getArr(s), n1, a)
- finitePoset(getVert(s), getArr(s))
+ dim : NNI := #(getVert(s))
+ mat := bll_to_mat(dim, getArr(s))
+ mat(n1, n2) := true
+ transitive_closure!(mat)
+ not(anitsymmetric?(mat)) =>
+ error "addArrow!: incompatible arrow"
+ finitePoset(getVert(s), mat_to_bll(mat))
-- local function to test a single value in the arrow matrix
isArrow?(arr : List(List(Boolean)), a : NNI, b : NNI) : Boolean ==
- row : NNI := 1
- for x in arr repeat
- if row = a then
- val : Boolean := qelt(x, b)
- return val
- row = row + 1
- false
+ qelt(qelt(arr, a), b)
le(s : %, a : NNI, b : NNI) : Boolean == isArrow?(getArr(s), a, b)
- -- local function to set a single value in the arrow matrix
- setArrow!(arr : List(List(Boolean)), a : NNI, b : NNI, c : Boolean
- ) : Void ==
- row : NNI := 1
- for x in arr repeat
- if row = a then
- setelt!(x, b, c)
- return void
- row = row + 1
- void
-
-- start of FiniteGraph implementation
- -- addObject!(s, n) adds object n to the graph s.
- -- mutable version of addObject.
- addObject!(s : %, n : S) : % ==
- dim : NNI := #(getVert(s)) + 1
- obs : List S := concat(getVert(s), n)
- arrows := []$List(List(Boolean))
- for a in getArr(s) repeat
- width : NNI := #a
- padding : Union(NNI, "failed") := subtractIfCan(dim, width)
- if padding ~= "failed" then
- diff : NNI := padding::NNI
- --print("addObject! diff="::Symbol << string(diff))
- for x in 1..diff repeat
- a := concat(a, false)
- if empty?(arrows)
- then arrows := [a]
- else arrows := concat(arrows, a)
- emptyRow : List Boolean := [false for x in 1..dim]
- arrows := concat(arrows, emptyRow)
- setVert(s, obs)
- setArr(s, arrows)
- s
-
-- addObject!(s, n) adds object with coordinates n to the
-- graph s.
addObject!(s : %, n : OBJT) : % ==
@@ -871,10 +840,7 @@ Poset(S) : Category == Definition where
-- n1 is the index of the start object
-- n2 is the index of the end object
addArrow!(s : %, name : String, n1 : NNI, n2 : NNI) : % ==
- a : List Boolean := qelt(getArr(s), n1)
- setelt!(a, n2, true)
- setelt!(getArr(s), n1, a)
- finitePoset(getVert(s), getArr(s))
+ addArrow!(s, n1, n2)
-- addArrow!(s, nm, n1, n2, mp) adds an arrow to the graph s, where:
-- nm is the name of the arrow
@@ -899,8 +865,8 @@ Poset(S) : Category == Definition where
arr : ARROW := ["x", 0::NNI, x pretend NNI,
y pretend NNI, 0::Integer, 0::Integer,
[]$List(NNI)]
- res := concat(res, arr)
- res
+ res := cons(arr, res)
+ reverse!(res)
-- flatten(n) takes a second order graph, we don't really need
-- this here so return an empty poset.
@@ -942,12 +908,9 @@ Poset(S) : Category == Definition where
unit(objs : List(S), arrowName : String) : % ==
dim : NNI := #objs
arrs : List(List(Boolean)) := [[]$List(Boolean)]
- for x in 1..dim repeat
- row : List Boolean := []
- for y in 1..dim repeat
- val : Boolean := (x = y)
- row := concat(row, val)
- arrs := concat(arrs, row)
+ for i in dim..1 by -1 repeat
+ row : List(Boolean) := [i = j for j in 1..dim]
+ arrs := cons(row, arrs)
finitePoset(objs, arrs)
-- kgraph(objs, arrowName)
@@ -1172,15 +1135,12 @@ Poset(S) : Category == Definition where
-- all the arrows
opposite(s : %) : % ==
arr2 : List List Boolean := [[]]
- for x in getArr(s) repeat
- row : List Boolean := []
- for y in x repeat
- row := concat(row, false)
- arr2 := concat(arr2, row)
- for a in 1..#(getArr(s)) repeat
- for b in 1..#(getArr(s)) repeat
- if isArrow?(getArr(s), a, b) then setArrow!(arr2, b, a, true)
- finitePoset(getVert(s), arr2)
+ dim : NNI := #getVert(s)
+ mat := new(dim, dim, false)$TwoDimensionalArray(Boolean)
+ for row in getArr(s) for i in 1.. repeat
+ for y in row for j in 1.. repeat
+ mat(j, i) := y
+ finitePoset(getVert(s), mat_to_bll(mat))
implies(s : %, left : NNI, right : NNI) : Boolean ==
a : List Boolean := qelt(getArr(s), left)
@@ -1335,42 +1295,6 @@ Poset(S) : Category == Definition where
objectToIndex(s : %, obj : S) : NNI ==
position(obj, getVert(s))$List(S) pretend NNI
- -- Reflexivity requires forall(x): x<=x
- -- This function enforces this by making sure that every element has
- -- arrow to itself. That is, the leading diagonal is true.
- completeReflexivity(s : %) : % ==
- set2 : List S := getVert(s)
- struct2 : List(List(Boolean)) := copy(getArr(s))
- for a in 1..(#set2) repeat
- setArrow!(struct2, a, a, true)
- finitePoset(set2, struct2)
-
- -- Transitivity requires forall(x, y, z): x<=y and y<=z implies x<=z
- -- This function enforces this by making sure that the composition
- -- of any two arrows is also an arrow.
- completeTransitivity(s : %) : % ==
- set2 : List S := getVert(s)
- dim : NNI := #set2
- struct2 : List(List(Boolean)) := copy(getArr(s))
- for a in 1..dim repeat
- for b in 1..dim repeat
- for c in 1..dim repeat
- if isArrow?(struct2, a, b) and isArrow?(struct2, b, c)
- and not(isArrow?(struct2, a, c)) then
- setArrow!(struct2, a, c, true)
- finitePoset(set2, struct2)
-
- -- Antisymmetric requires forall(x, y): x<=y and y<=x iff x=y
- -- Returns true if this is the case for every element.
- isAntisymmetric?(s : %) : Boolean ==
- dim : NNI := #(getVert(s))
- struct2 : List(List(Boolean)) := copy(getArr(s))
- for a in 1..dim repeat
- for b in 1..dim repeat
- if isArrow?(struct2, a, b) and isArrow?(struct2, b, a) then
- if a ~= b then return false
- true
-
-- \spad{zetaMatrix(P)} returns the matrix of the zeta function
-- This function is based on code by Franz Lehner.
zetaMatrix(s : %) : IncidenceAlgebra(Integer, S) ==
