Hi Konrad, Thank you very much! I’m learning finite_mapTheory now.
Regards, Chun > Il giorno 23 ott 2017, alle ore 20:42, Konrad Slind <konrad.sl...@gmail.com> > ha scritto: > > Hi Chun Tian, > > There are all kinds of issues with substitutions and applying them to > term-like > structures. I would probably start by choosing finite maps (finite_mapTheory) > as > the representation for variable substitutions since they get rid of most if > not all > the issues with ordering of replacements. The alistTheory provides a more > computationally friendly version, and provides a formal connection back to > fmaps. > > Also see > > <holdir>/examples/unification/triangular/first-order > > for a unification case study. > > Konrad. > > > On Mon, Oct 23, 2017 at 10:48 AM, Chun Tian <binghe.l...@gmail.com> wrote: > 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 > > > ------------------------------------------------------------------------------ > 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 > >
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
