Hi, Suppose I have a list (or recursive structure defined by Datatype) in which there’re some special elements marked as “variables”, e.g. ``var X``, ``var Y``, … and I have a substitution function which correctly replaces a variable into another closed term (i.e. term without variables), and an extended version of this function can do repeated variable substitutions on a list of variables and their corresponding substitutions. E.g. ``SUBST E Ps Xs`` will do substitutions in list of strings E, finding each appearance of variable in Xs and replace with the corresponding one in Ps. The type of SUBST should be something like ``:string list -> string list -> string list -> string list``.
I can imagine that, for whatever permutations of Xs (or the order of variables), with Ps also changed in the same order, the resulting term ``SUBST Es Ps Xs`` must be unique. (if Ps also contains variables, the resulting term may not be unique any more.) How can expression this property (e.g. in listTheory)? What’s the name of this phenomena? and what’s the idea in its proof? Regards, Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
