\documentclass{article} \usepackage{open-axiom} \begin{document} \title{\$SPAD/src/algebra newdata.spad} \author{Themos Tsikas, Marc Moreno Maza} \maketitle \begin{abstract} \end{abstract} \eject \tableofcontents \eject \section{package IPRNTPK InternalPrintPackage} <>= )abbrev package IPRNTPK InternalPrintPackage ++ Author: Themos Tsikas ++ Date Created: 09/09/1998 ++ Date Last Updated: 09/09/1998 ++ Basic Functions: ++ Related Constructors: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ References: ++ Description: A package to print strings without line-feed ++ nor carriage-return. InternalPrintPackage(): Exports == Implementation where Exports == with iprint: String -> Void ++ \axiom{iprint(s)} prints \axiom{s} at the current position ++ of the cursor. Implementation == add iprint(s:String) == PRINC(coerce(s)@Symbol)$Lisp FORCE_-OUTPUT()$Lisp @ \section{package TBCMPPK TabulatedComputationPackage} <>= )abbrev package TBCMPPK TabulatedComputationPackage ++ Author: Marc Moreno Maza ++ Date Created: 09/09/1998 ++ Date Last Updated: 12/16/1998 ++ Basic Functions: ++ Related Constructors: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ References: ++ Description: ++ \axiom{TabulatedComputationPackage(Key ,Entry)} provides some modest support ++ for dealing with operations with type \axiom{Key -> Entry}. The result of ++ such operations can be stored and retrieved with this package by using ++ a hash-table. The user does not need to worry about the management of ++ this hash-table. However, onnly one hash-table is built by calling ++ \axiom{TabulatedComputationPackage(Key ,Entry)}. ++ Version: 2. TabulatedComputationPackage(Key ,Entry): Exports == Implementation where Key: SetCategory Entry: SetCategory N ==> NonNegativeInteger H ==> HashTable(Key, Entry, "EQUAL") iprintpack ==> InternalPrintPackage() Exports == with initTable!: () -> Void ++ \axiom{initTable!()} initializes the hash-table. printInfo!: (String, String) -> Void ++ \axiom{printInfo!(x,y)} initializes the mesages to be printed ++ when manipulating items from the hash-table. If ++ a key is retrieved then \axiom{x} is displayed. If an item is ++ stored then \axiom{y} is displayed. startStats!: (String) -> Void ++ \axiom{startStats!(x)} initializes the statisitics process and ++ sets the comments to display when statistics are printed printStats!: () -> Void ++ \axiom{printStats!()} prints the statistics. clearTable!: () -> Void ++ \axiom{clearTable!()} clears the hash-table and assumes that ++ it will no longer be used. usingTable?: () -> Boolean ++ \axiom{usingTable?()} returns true iff the hash-table is used printingInfo?: () -> Boolean ++ \axiom{printingInfo?()} returns true iff messages are printed ++ when manipulating items from the hash-table. makingStats?: () -> Boolean ++ \axiom{makingStats?()} returns true iff the statisitics process ++ is running. extractIfCan: Key -> Union(Entry,"failed") ++ \axiom{extractIfCan(x)} searches the item whose key is \axiom{x}. insert!: (Key, Entry) -> Void ++ \axiom{insert!(x,y)} stores the item whose key is \axiom{x} and whose ++ entry is \axiom{y}. Implementation == add table?: Boolean := false t: H := empty() info?: Boolean := false stats?: Boolean := false used: NonNegativeInteger := 0 ok: String := "o" ko: String := "+" domainName: String := empty()$String initTable!(): Void == table? := true t := empty() printInfo!(s1: String, s2: String): Void == (empty? s1) or (empty? s2) => void() not usingTable?() => error "in printInfo!()$TBCMPPK: not allowed to use hashtable" info? := true ok := s1 ko := s2 startStats!(s: String): Void == empty? s => void() not table? => error "in startStats!()$TBCMPPK: not allowed to use hashtable" stats? := true used := 0 domainName := s printStats!(): Void == not table? => error "in printStats!()$TBCMPPK: not allowed to use hashtable" not stats? => error "in printStats!()$TBCMPPK: statistics not started" output(" ")$OutputPackage title: String := concat("*** ", concat(domainName," Statistics ***")) output(title)$OutputPackage n: N := #t output(" Table size: ", n::OutputForm)$OutputPackage output(" Entries reused: ", used::OutputForm)$OutputPackage clearTable!(): Void == not table? => error "in clearTable!()$TBCMPPK: not allowed to use hashtable" t := empty() table? := false info? := false stats? := false domainName := empty()$String usingTable?() == table? printingInfo?() == info? makingStats?() == stats? extractIfCan(k: Key): Union(Entry,"failed") == not table? => "failed" :: Union(Entry,"failed") s := search(k,t) s case Entry => if info? then iprint(ok)$iprintpack if stats? then used := used + 1 return s "failed" :: Union(Entry,"failed") insert!(k: Key, e:Entry): Void == not table? => void() t.k := e if info? then iprint(ko)$iprintpack @ \section{domain SPLNODE SplittingNode} <>= )abbrev domain SPLNODE SplittingNode ++ Author: Marc Moereno Maza ++ Date Created: 07/05/1996 ++ Date Last Updated: 07/19/1996 ++ Basic Functions: ++ Related Constructors: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ References: ++ References: ++ Description: ++ This domain exports a modest implementation for the ++ vertices of splitting trees. These vertices are called ++ here splitting nodes. Every of these nodes store 3 informations. ++ The first one is its value, that is the current expression ++ to evaluate. The second one is its condition, that is the ++ hypothesis under which the value has to be evaluated. ++ The last one is its status, that is a boolean flag ++ which is true iff the value is the result of its ++ evaluation under its condition. Two splitting vertices ++ are equal iff they have the sane values and the same ++ conditions (so their status do not matter). SplittingNode(V,C) : Exports == Implementation where V:Join(SetCategory,Aggregate) C:Join(SetCategory,Aggregate) Z ==> Integer B ==> Boolean O ==> OutputForm VT ==> Record(val:V, tower:C) VTB ==> Record(val:V, tower:C, flag:B) Exports == SetCategory with empty : () -> % ++ \axiom{empty()} returns the same as ++ \axiom{[empty()$V,empty()$C,false]$%} empty? : % -> B ++ \axiom{empty?(n)} returns true iff the node n is \axiom{empty()$%}. value : % -> V ++ \axiom{value(n)} returns the value of the node n. condition : % -> C ++ \axiom{condition(n)} returns the condition of the node n. status : % -> B ++ \axiom{status(n)} returns the status of the node n. construct : (V,C,B) -> % ++ \axiom{construct(v,t,b)} returns the non-empty node with ++ value v, condition t and flag b construct : (V,C) -> % ++ \axiom{construct(v,t)} returns the same as ++ \axiom{construct(v,t,false)} construct : VT -> % ++ \axiom{construct(vt)} returns the same as ++ \axiom{construct(vt.val,vt.tower)} construct : List VT -> List % ++ \axiom{construct(lvt)} returns the same as ++ \axiom{[construct(vt.val,vt.tower) for vt in lvt]} construct : (V, List C) -> List % ++ \axiom{construct(v,lt)} returns the same as ++ \axiom{[construct(v,t) for t in lt]} copy : % -> % ++ \axiom{copy(n)} returns a copy of n. setValue! : (%,V) -> % ++ \axiom{setValue!(n,v)} returns n whose value ++ has been replaced by v if it is not ++ empty, else an error is produced. setCondition! : (%,C) -> % ++ \axiom{setCondition!(n,t)} returns n whose condition ++ has been replaced by t if it is not ++ empty, else an error is produced. setStatus!: (%,B) -> % ++ \axiom{setStatus!(n,b)} returns n whose status ++ has been replaced by b if it is not ++ empty, else an error is produced. setEmpty! : % -> % ++ \axiom{setEmpty!(n)} replaces n by \axiom{empty()$%}. infLex? : (%,%,(V,V) -> B,(C,C) -> B) -> B ++ \axiom{infLex?(n1,n2,o1,o2)} returns true iff ++ \axiom{o1(value(n1),value(n2))} or ++ \axiom{value(n1) = value(n2)} and ++ \axiom{o2(condition(n1),condition(n2))}. subNode? : (%,%,(C,C) -> B) -> B ++ \axiom{subNode?(n1,n2,o2)} returns true iff ++ \axiom{value(n1) = value(n2)} and ++ \axiom{o2(condition(n1),condition(n2))} Implementation == add Rep == VTB empty() == per [empty()$V,empty()$C,false]$Rep empty?(n:%) == empty?((rep n).val)$V and empty?((rep n).tower)$C value(n:%) == (rep n).val condition(n:%) == (rep n).tower status(n:%) == (rep n).flag construct(v:V,t:C,b:B) == per [v,t,b]$Rep construct(v:V,t:C) == [v,t,false]$% construct(vt:VT) == [vt.val,vt.tower]$% construct(lvt:List VT) == [[vt]$% for vt in lvt] construct(v:V,lt: List C) == [[v,t]$% for t in lt] copy(n:%) == per copy rep n setValue!(n:%,v:V) == (rep n).val := v n setCondition!(n:%,t:C) == (rep n).tower := t n setStatus!(n:%,b:B) == (rep n).flag := b n setEmpty!(n:%) == (rep n).val := empty()$V (rep n).tower := empty()$C n infLex?(n1,n2,o1,o2) == o1((rep n1).val,(rep n2).val) => true (rep n1).val = (rep n2).val => o2((rep n1).tower,(rep n2).tower) false subNode?(n1,n2,o2) == (rep n1).val = (rep n2).val => o2((rep n1).tower,(rep n2).tower) false -- sample() == empty() n1:% = n2:% == (rep n1).val ~= (rep n2).val => false (rep n1).tower = (rep n2).tower n1:% ~= n2:% == (rep n1).val = (rep n2).val => false (rep n1).tower ~= (rep n2).tower coerce(n:%):O == l1,l2,l3,l : List O l1 := [message("value == "), ((rep n).val)::O] o1 : O := blankSeparate l1 l2 := [message(" tower == "), ((rep n).tower)::O] o2 : O := blankSeparate l2 if ((rep n).flag) then o3 := message(" closed == true") else o3 := message(" closed == false") l := [o1,o2,o3] bracket commaSeparate l @ \section{domain SPLTREE SplittingTree} <>= )abbrev domain SPLTREE SplittingTree ++ Author: Marc Moereno Maza ++ Date Created: 07/05/1996 ++ Date Last Updated: May 16, 2013 ++ Basic Functions: ++ Related Constructors: ++ Also See: ++ AMS Classifications: ++ Keywords: ++ References: ++ M. MORENO MAZA "Calculs de pgcd au-dessus des tours ++ d'extensions simples et resolution des systemes d'equations ++ algebriques" These, Universite P.etM. Curie, Paris, 1997. ++ Description: ++ This domain exports a modest implementation of splitting ++ trees. Spliiting trees are needed when the ++ evaluation of some quantity under some hypothesis ++ requires to split the hypothesis into sub-cases. ++ For instance by adding some new hypothesis on one ++ hand and its negation on another hand. The computations ++ are terminated is a splitting tree \axiom{a} when ++ \axiom{status(value(a))} is \axiom{true}. Thus, ++ if for the splitting tree \axiom{a} the flag ++ \axiom{status(value(a))} is \axiom{true}, then ++ \axiom{status(value(d))} is \axiom{true} for any ++ subtree \axiom{d} of \axiom{a}. This property ++ of splitting trees is called the termination ++ condition. If no vertex in a splitting tree \axiom{a} ++ is equal to another, \axiom{a} is said to satisfy ++ the no-duplicates condition. The splitting ++ tree \axiom{a} will satisfy this condition ++ if nodes are added to \axiom{a} by mean of ++ \axiom{splitNodeOf!} and if \axiom{construct} ++ is only used to create the root of \axiom{a} ++ with no children. SplittingTree(V,C) : Exports == Implementation where V:Join(SetCategory,Aggregate) C:Join(SetCategory,Aggregate) B ==> Boolean O ==> OutputForm NNI ==> NonNegativeInteger VT ==> Record(val:V, tower:C) VTB ==> Record(val:V, tower:C, flag:B) S ==> SplittingNode(V,C) A ==> Record(root:S,subTrees:List(%)) Exports == Join(RecursiveAggregate S,FiniteAggregate S,ShallowlyMutableAggregate S) with extractSplittingLeaf : % -> Union(%,"failed") ++ \axiom{extractSplittingLeaf(a)} returns the left ++ most leaf (as a tree) whose status is false ++ if any, else "failed" is returned. updateStatus! : % -> % ++ \axiom{updateStatus!(a)} returns a where the status ++ of the vertices are updated to satisfy ++ the "termination condition". construct : S -> % ++ \axiom{construct(s)} creates a splitting tree ++ with value (i.e. root vertex) given by ++ \axiom{s} and no children. Thus, if the ++ status of \axiom{s} is false, \axiom{[s]} ++ represents the starting point of the ++ evaluation \axiom{value(s)} under the ++ hypothesis \axiom{condition(s)}. construct : (V,C, List %) -> % ++ \axiom{construct(v,t,la)} creates a splitting tree ++ with value (i.e. root vertex) given by ++ \axiom{[v,t]$S} and with \axiom{la} as ++ children list. construct : (V,C,List S) -> % ++ \axiom{construct(v,t,ls)} creates a splitting tree ++ with value (i.e. root vertex) given by ++ \axiom{[v,t]$S} and with children list given by ++ \axiom{[[s]$% for s in ls]}. construct : (V,C,V,List C) -> % ++ \axiom{construct(v1,t,v2,lt)} creates a splitting tree ++ with value (i.e. root vertex) given by ++ \axiom{[v,t]$S} and with children list given by ++ \axiom{[[[v,t]$S]$% for s in ls]}. conditions : % -> List C ++ \axiom{conditions(a)} returns the list of the conditions ++ of the leaves of a result : % -> List VT ++ \axiom{result(a)} where \axiom{ls} is the leaves list of \axiom{a} ++ returns \axiom{[[value(s),condition(s)]$VT for s in ls]} ++ if the computations are terminated in \axiom{a} else ++ an error is produced. nodeOf? : (S,%) -> B ++ \axiom{nodeOf?(s,a)} returns true iff some node of \axiom{a} ++ is equal to \axiom{s} subNodeOf? : (S,%,(C,C) -> B) -> B ++ \axiom{subNodeOf?(s,a,sub?)} returns true iff for some node ++ \axiom{n} in \axiom{a} we have \axiom{s = n} or ++ \axiom{status(n)} and \axiom{subNode?(s,n,sub?)}. remove : (S,%) -> % ++ \axiom{remove(s,a)} returns the splitting tree obtained ++ from a by removing every sub-tree \axiom{b} such ++ that \axiom{value(b)} and \axiom{s} have the same ++ value, condition and status. remove! : (S,%) -> % ++ \axiom{remove!(s,a)} replaces a by remove(s,a) splitNodeOf! : (%,%,List(S)) -> % ++ \axiom{splitNodeOf!(l,a,ls)} returns \axiom{a} where the children ++ list of \axiom{l} has been set to ++ \axiom{[[s]$% for s in ls | not nodeOf?(s,a)]}. ++ Thus, if \axiom{l} is not a node of \axiom{a}, this ++ latter splitting tree is unchanged. splitNodeOf! : (%,%,List(S),(C,C) -> B) -> % ++ \axiom{splitNodeOf!(l,a,ls,sub?)} returns \axiom{a} where the children ++ list of \axiom{l} has been set to ++ \axiom{[[s]$% for s in ls | not subNodeOf?(s,a,sub?)]}. ++ Thus, if \axiom{l} is not a node of \axiom{a}, this ++ latter splitting tree is unchanged. Implementation == add Rep == A construct(s:S) == per [s,[]]$A construct(v:V,t:C,la:List(%)) == per [[v,t]$S,la]$A construct(v:V,t:C,ls:List(S)) == per [[v,t]$S,[[s]$% for s in ls]]$A construct(v1:V,t:C,v2:V,lt:List(C)) == [v1,t,([v2,lt]$S)@(List S)]$% empty?(a:%) == empty?((rep a).root) and empty?((rep a).subTrees) empty() == [empty()$S]$% remove(s:S,a:%) == empty? a => a (s = value(a)) and (status(s) = status(value(a))) => empty()$% la := children(a) lb : List % := [] while (not empty? la) repeat lb := cons(remove(s,first la), lb) la := rest la lb := reverse remove(empty?,lb) [value(value(a)),condition(value(a)),lb]$% remove!(s:S,a:%) == empty? a => a (s = value(a)) and (status(s) = status(value(a))) => (rep a).root := empty()$S (rep a).subTrees := [] a la := children(a) lb : List % := [] while (not empty? la) repeat lb := cons(remove!(s,first la), lb) la := rest la lb := reverse remove(empty()$%,lb) setchildren!(a,lb) value(a:%) == (rep a).root children(a:%) == (rep a).subTrees leaf?(a:%) == empty? a => false empty? (rep a).subTrees setchildren!(a:%,la:List(%)) == (rep a).subTrees := la a setvalue!(a:%,s:S) == (rep a).root := s s cyclic?(a:%) == false map(foo:(S -> S),a:%) == empty? a => a b : % := [foo(value(a))]$% leaf? a => b setchildren!(b,[map(foo,c) for c in children(a)]) map!(foo:(S -> S),a:%) == empty? a => a setvalue!(a,foo(value(a))) leaf? a => a setchildren!(a,[map!(foo,c) for c in children(a)]) copy(a:%) == map(copy,a) eq?(a1:%,a2:%) == error"in eq? from SPLTREE : la vache qui rit est-elle folle?" nodes(a:%) == empty? a => [] leaf? a => [a] cons(a,concat([nodes(c) for c in children(a)])) leaves(a:%) == empty? a => [] leaf? a => [value(a)] concat([leaves(c) for c in children(a)]) members(a:%) == empty? a => [] leaf? a => [value(a)] cons(value(a),concat([members(c) for c in children(a)])) #(a:%) == empty? a => 0$NNI leaf? a => 1$NNI reduce("+",[#c for c in children(a)],1$NNI)$(List NNI) a1:% = a2:% == empty? a1 => empty? a2 empty? a2 => false leaf? a1 => not leaf? a2 => false value(a1) =$S value(a2) leaf? a2 => false value(a1) ~=$S value(a2) => false children(a1) = children(a2) -- sample() == [sample()$S]$% localCoerce(a:%,k:NNI):O == s : String if k = 1 then s := "* " else s := "-> " for i in 2..k repeat s := concat("-+",s)$String ro : O := left(hconcat(message(s)$O,value(a)::O)$O)$O leaf? a => ro lo : List O := [localCoerce(c,k+1) for c in children(a)] lo := cons(ro,lo) vconcat(lo)$O coerce(a:%):O == empty? a => vconcat(message(" ")$O,message("* []")$O) vconcat(message(" ")$O,localCoerce(a,1)) extractSplittingLeaf(a:%) == empty? a => "failed"::Union(%,"failed") status(value(a))$S => "failed"::Union(%,"failed") la := children(a) empty? la => a while (not empty? la) repeat esl := extractSplittingLeaf(first la) (esl case %) => return(esl) la := rest la "failed"::Union(%,"failed") updateStatus!(a:%) == la := children(a) (empty? la) or (status(value(a))$S) => a done := true while (not empty? la) and done repeat done := done and status(value(updateStatus! first la)) la := rest la setStatus!(value(a),done)$S a result(a:%) == empty? a => [] not status(value(a))$S => error"in result from SLPTREE : mad cow!" ls : List S := leaves(a) [[value(s),condition(s)]$VT for s in ls] conditions(a:%) == empty? a => [] ls : List S := leaves(a) [condition(s) for s in ls] nodeOf?(s:S,a:%) == empty? a => false s =$S value(a) => true la := children(a) while (not empty? la) and (not nodeOf?(s,first la)) repeat la := rest la not empty? la subNodeOf?(s:S,a:%,sub?:((C,C) -> B)) == empty? a => false -- s =$S value(a) => true status(value(a)$%)$S and subNode?(s,value(a),sub?)$S => true la := children(a) while (not empty? la) and (not subNodeOf?(s,first la,sub?)) repeat la := rest la not empty? la splitNodeOf!(l:%,a:%,ls:List(S)) == ln := removeDuplicates ls la : List % := [] while not empty? ln repeat if not nodeOf?(first ln,a) then la := cons([first ln]$%, la) ln := rest ln la := reverse la setchildren!(l,la)$% if empty? la then (rep l).root := [empty()$V,empty()$C,true]$S updateStatus!(a) splitNodeOf!(l:%,a:%,ls:List(S),sub?:((C,C) -> B)) == ln := removeDuplicates ls la : List % := [] while not empty? ln repeat if not subNodeOf?(first ln,a,sub?) then la := cons([first ln]$%, la) ln := rest ln la := reverse la setchildren!(l,la)$% if empty? la then (rep l).root := [empty()$V,empty()$C,true]$S updateStatus!(a) @ \section{License} <>= --Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. --All rights reserved. -- Copyright (C) 2007-2010, Gabriel Dos Reis -- All rights reserved. -- --Redistribution and use in source and binary forms, with or without --modification, are permitted provided that the following conditions are --met: -- -- - Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- -- - Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in -- the documentation and/or other materials provided with the -- distribution. -- -- - Neither the name of The Numerical ALgorithms Group Ltd. nor the -- names of its contributors may be used to endorse or promote products -- derived from this software without specific prior written permission. -- --THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS --IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED --TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A --PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER --OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, --EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, --PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR --PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF --LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING --NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS --SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. @ <<*>>= <> <> <> <> <> @ \eject \begin{thebibliography}{99} \bibitem{1} nothing \end{thebibliography} \end{document}