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
> 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
>
> /examples/unification/triangular/first-order
>
> for a unification case study.
>
> Konrad.
>
>
> On Mon, Oct 23, 2017 at 10:48 AM, Chun Tian 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
