Thread: Any smart guys here (substitutions)?

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?

A small typo in the above result. The result should (obviously) be:

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?

Originally Posted by emakarov

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

Originally Posted by emakarov

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

Awesome! I'm so glad you took time to elaborate this. This notation is both concise and intuitive!

Thanks very much!