A small typo in the above result. The result should (obviously) be:
Hi,
I have a question on how to "combine" substitutions in the sense that there is a dependency between two kinds of substitutions. I'll try to concretise this in an example.
I have a structure consisting of a pair:
where
is merely a set of labels composed from small letters.
Examples of are:
is the power set of
Moreover, there are two types of substitutions, A and B:
Substitutions of type A work on the first element of an element of , while substitutions of type B work on the second element of .
represents the dependency between substitutions of type A and B. That is, they are grouped in pairs.
What I wonder is how to define and apply these substitutions correctly to achieve the following:
| represents the action\operator that applies the substitutions correctly. That is, the substitutions of type B (second element of S) is only applied if the substitution of type A (first element of S) is applied.
Any ideas?
What do you want to get: a strict mathematical description, code in some programming language or something else?
I would start by defining the result of applying a substitution of type B to a set.
An important issue is when s = {<a1,b1>, <a2,b2>}, y = {x} and both a1 and a2 are applicable to the first element of x. What happens then?
Thanks very much for your response! Appreciated!
I'm trying to come up with a concise mathematical notation that describes the "combined" action of the substitutions. That said, I'm not sure how to do this in a "proper" way. Obviously, I could write a textual description telling how the desired result should be, but I prefer a pure mathematical notation with less text. For instance, I'm not sure how to define application of several substitutions which are found in a set. That is, if I have a set of substitutions, how can I apply all of these substitutions to a structure. Let's say
Could I do something like this:
And does this mean that all substitutions of b are "carried out" resulting in x (where labels are changed).
The case you refer to where two A substititons match the first element of X should not be legal.
First, I should note that I encountered the term "substitution" only when a variable occurring in a syntactic expression is replaced by another expression. For example, if E = x^2 = x + 1 and ϴ = [x ↦ 2 + 3] is substitution, then Eϴ = (2 + 3)^2 = (2 + 3) + 1. It is customary to denote substitutions by Greek letters and denote the result of the application by Eϴ or ϴ(E).
Let u range over elements of L and w range over subsets of L. We can identify the set of substitutions A with L x L, i.e., the set of pairs of elements of L, and B with the set of functions from L to L. If f ∊ B and w ⊆ L, it is customary to denote {f(u) | u ∊ w} by f[w].
So, let y ∊ Y and s ∊ S. Define y | s, or s(y), to be
{<a', f[w]> | <a, w> ∊ y, <<a, a'>, f> ∊ s} ∪
{<a, w> | <a, w> ∊ y, <<a, a'>, f> ∉ s for all a', f}.
The second set in the union corresponds to those pairs x whose first element is not subject to a substitution from y, if this is possible. To prove that y | s is well-defined one has to show that it is impossible that <a, w> ∊ y and <<a, a'>, f'> ∊ s, <<a, a''>, f''> ∊ s for a' ≠ a'' or f' ≠ f''.