OKlibrary  0.2.1.6
ConstraintTemplateRewriteSystem.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.9.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 
00024 /* ********************************************
00025    * Rewrite system functions                 *
00026    ********************************************
00027 */
00028 
00029 /* The idea is that the arguments should uniquely identify a given constraint
00030    within the context of its parent constraint and therefore, as its
00031    parent constraint is uniquely identified above, we have inductively
00032    that any variable is uniquely identified.
00033 
00034    The five main data types represented below are "namespaces", "constraint
00035    templates", "rewrite bundles", "rewrite maps" and
00036    "constraint template rewrite rules".
00037 
00038    A "namespace" is a function which takes a variable and returns a
00039    variable. This function need not actually evaluate, and in fact, this
00040    is precisely the point in the majority of cases. For the standard 
00041    namespaces constructed in this system see cstt_namespace_new.
00042 
00043    As the output type of any namespace function is a variable, the function
00044    should be declared posfun and noun if it is not evaluated.
00045 
00046    A "constraint template" is a list of at least three elements, where the
00047    first element is the name of the constraint template, the second element is
00048    the list of variables associated with the constraint template and the last
00049    (note, not the third) is the namespace of the function. A constraint
00050    template may optionally have any number of arguments situated in between
00051    it's 2nd and last elements which will relate to the working of each
00052    constraint template.
00053 
00054    A "constraint template rewrite rule" is a function which takes a constraint
00055    template and returns a list of constraint templates which model the input
00056    constraint template. Note here that new variables can be introduced using
00057    the namespace of the original constraint template composed with a new
00058    namespace constructed for the new constraint templates. 
00059 
00060    A "rewrite bundle" is a list with two elements, where the first element
00061    is a constraint template rewrite rule f, and the second element is a 
00062    function which, given a constraint template, returns a list of
00063    variables introduced by f. 
00064 
00065    A "constraint rewrite map" is a an ordered set map which maps
00066    a given constraint template name to a rewrite bundle.
00067  
00068    For examples see docus/ConstraintTemplateRewriteSystem.hpp.
00069 */
00070 
00071 
00072 /****************************
00073  * Namespaces               *
00074  ****************************
00075 */
00076 
00077 /* Given a parent namespace namespace_p, a new unevaluated function
00078    namespace_name, and a constraint cst_p, returns a new namespace, which
00079    consists of namespace_p composed with the namespace_name, where elements
00080    of cst_p are used as additional arguments to namespace_p to create a
00081    unique namespace in the context of the given constraint template.
00082 
00083    Note here all elements of the constraint template *except the variables*
00084    are used to uniquely identify the namespace. The variables are not used
00085    as in any non-trivial system where there are multiple levels of namespaces,
00086    and many variables at each level, one would (and experimentally does)
00087    encounter exponential blow-up in the size of the namespace terms. Therefore
00088    any constraint template given should be uniquely identifiable using only
00089    it's name, arguments and namespace, and should not require the variables to
00090    be unique.
00091 */
00092 cstt_namespace_new(namespace_name,cst_p) := block([namespace_p,res_cstt_p],
00093   namespace_p :
00094     if list_p(cst_p) and length(cst_p) < 3 then cstt_id_ns else last(cst_p),
00095   res_cstt_p : append([cstt_name(cst_p)],cstt_args_l(cst_p), [cstt_namespace_f(cst_p)]),
00096   return(buildq([res_cstt_p,namespace_name,namespace_p],
00097         lambda([a],namespace_p(namespace_name(a,res_cstt_p))))))$
00098 
00099 
00100 /* Given a constraint and a namespace, returns a new constraint
00101    with all the same properties of the input constraint except
00102    the namespace has been composed with the input namespace. */
00103 cstt_namespace_replace(cstt, namespace) :=
00104   append(rest(cstt,-1), [namespace])$
00105 
00106 
00107 /* Namespace which acts as the identity on the given variable: */
00108 cstt_id_ns(a) := a$
00109 
00110 
00111 /****************************
00112  * Constraints              *
00113  ****************************
00114 */
00115 
00116 /* Given a constraint name, a list of variables in the constraint, a list
00117    of constraint parameters and a namespace, ???
00118    returns a constraint template constructed from these parameters. */
00119 cstt_new(cst_n,vars,arg_l,namespace) :=
00120   append([cst_n,vars],arg_l,[namespace])$
00121 
00122 /* Given a constraint template returns the constraint template name. ??? */
00123 cstt_name(cst) := first(cst)$
00124 
00125 /* Given a constraint template returns the variables in the constraint
00126    template ??? */
00127 cstt_vars_l(cst) :=
00128   if listp(cst) and length(cst) > 1 and listp(cst[2]) then second(cst) else []$
00129 
00130 /* Given a constraint template returns the constraint template
00131    auxiliary arguments. ??? */
00132 cstt_args_l(cst) :=
00133   if listp(cst) and length(cst) > 3 then rest(rest(cst,2),-1) else []$
00134 
00135 /* Given a constraint template returns the namespace of the constraint
00136    template. ??? */
00137 cstt_namespace_f(cst) :=
00138   if listp(cst) and length(cst) > 3 then last(cst) else cstt_id_ns$
00139 
00140 /* Check whether a given object is a constraint template ??? */
00141 cstt_p(cstt) := is(listp(cstt) and length(cstt) >= 2)$
00142 
00143 /* Check whether a given object is a constraint template with
00144    the given name ??? */
00145 cstt_named_p(cstt,name) := is(cstt_p(cstt) and cstt[1] = name)$
00146 
00147 
00148 /* Given a constraint template, a list of variables from the constraint
00149    and another list of variables, returns the new constraint where
00150    the variables in the first list have been replaced with the second. */
00151 cstt_rename_vars(cstt, old_var_l, new_var_l) := if not(cstt_p(cstt)) then []
00152   else block([var_map : sm2hm(setify(map("[",old_var_l, new_var_l)))],
00153     append([cstt[1]],
00154            [map(lambda([a], if ev_hm(var_map,a) # false then
00155                  ev_hm(var_map,a) else a), cstt[2])],
00156            rest(cstt,2)))$
00157 cstt_rename_wsm_vars(cstt, var_map) :=
00158   if not(cstt_p(cstt)) then [] else
00159   append(
00160     [cstt[1], map(lambda([a], ev_hm_d(var_map,a,a)), cstt[2])],
00161            rest(cstt,2))$
00162 cstt_rename_wsm_vars_ip(cstt, var_map) :=
00163   if not(cstt_p(cstt)) then [] else
00164   cstt[2] : map(lambda([a], ev_hm_d(var_map,a,a)), cstt[2])$
00165 
00166 csttl_rename_vars(csttl, old_var_l, new_var_l) := block(
00167   [var_map : sm2hm(map("[",old_var_l, new_var_l))],
00168   map(lambda([cstt], cstt_rename_wsm_vars(cstt, var_map)), csttl))$
00169 
00170 csttl_rename_vars_ip(csttl, old_var_l, new_var_l) := block(
00171   [var_map : sm2hm(map("[",old_var_l, new_var_l))],
00172   for i : 1 thru length(csttl) do cstt_rename_wsm_vars_ip(csttl[i],var_map))$
00173 
00174 
00175 /********************************
00176  * Rewrite functions            *
00177  ********************************
00178 */
00179 
00180 /* Given a list of constraint templates, and a rewrite map, returns a new list
00181    of constraint templates after applying the given rewrite map. */
00182 rewrite_all_csttl(cstl,rewrite_map) := block(
00183   [rewrite_hash : osm2hm(rewrite_map),cstl_new : []],
00184   for cst in cstl do block([cstr],
00185     cstr : ev_hm(rewrite_hash,cst[1]),
00186     if cstr # false then
00187       cstl_new : cons(rewrite_all_csttl(cstr[1](cst),rewrite_map),cstl_new)
00188     else 
00189       cstl_new : cons([first(cstl)],cstl_new),
00190     cstl : rest(cstl)),
00191   return(lappend(cstl_new)))$
00192 
00193 /* Given a list of constraint templates, and a rewrite map, returns a list of
00194    new variables which would be introduced when calling rewrite_all
00195    with the same parameters. */
00196 rewrite_all_cstt_vars_l(cstl,rewrite_map) := block(
00197     [rewrite_hash : osm2hm(rewrite_map),lookup_var_lf,varl : []],
00198     lookup_var_lf : lambda([cst], block(
00199         [rwf : ev_hm_d(rewrite_hash,cst[1],zero_csttrb)],
00200         append(
00201           rwf[3](cst),
00202           rewrite_all_cstt_vars_l(rwf[1](cst),rewrite_map)))),
00203     return(lappend(map(lookup_var_lf,cstl))))$
00204 
00205 
00206 /****************************************
00207  * Rewrite bundles                      *
00208  ****************************************
00209 */
00210 
00211 /* Constraint template rewrite bundle which does nothing
00212    (i.e the rewrite function it represents has the identity
00213    as it's namespace, and no variables are introduced by it's
00214    rewrite function). */
00215 zero_csttrb : [lambda([[a]],[]), cstt_id_ns,lambda([[a]],[])]$
00216