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
>
>
------------------------------------------------------------------------------
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
