Thread: Substitution and composition of functions

Hi all,

I've recently encountered a notational difficulty regarding functions and compositions in which I do not have the competence to solve. Hopefully, there are some people here that may give some hints or advices. I truly appreciate any effort!

I've linked to a provisional formalisation with this post, so hopefully you will have a better understanding of the problem. Note, however, that this is just an attempt and it is probably not correct. You can find this early attempt here: notation.png - File Shared from Box.net - Free Online File Storage

As the title suggests, I would like to perform substitutions on a structure. For simplicity, this structure is here a 2-tuple of type 'C'. Each substitution is described by a (partial) function of type 'F'. Specifically, I would like to be able to successively perform substitutions on this tuple, as described by a set of substitutions (function space).

A C-tuple comprises two elements; one of type 'I' and one of type 'T'. 'I' can be seen as a set of labels 'a, b, ..., z' while 'T' is irrelevant for this shortened example. Moreover, the possible substitutions are listed in 'F'. A substitution 'f' (of 'F') is defined from 'I x I x C' to 'C'. That is, it takes two labels and one C-tuple as arguments and produces a new C-tuple. This C-tuple is identical to the provided (argument) tuple with the exception that a substitution of its first element may have occurred ('I -> I'). Please see the linked description for a full definition of 'f' and some examples.

At this point there is an inconsistency in my attempt, so it may look a little confusing. I've explicitly defined a function 'f' that defines the nature of a substitution. However, the definition of 'f' should apply to all functions of 'F' since they all act the same. The only difference between them is the 'from' and 'to' subscripts. Finally, there is a function 'g' that performs the substitutions found in 'fx' on a tuple 'c' - both given as arguments.

My questions are:

1. Will the substitutions actually be partial functions from 'I x I x C' to 'C' (or mayby from 'C' to 'C'?), where the subscripts dictate when a substitution should be performed?

2. Is this kind of subscripting legal, and will the substitutions be legal partial functions?

3. Can I use one definition for a function 'f' (as done) to describe the nature of all substitutions of 'F' (and refer to the subscripts in the function definition as x, y or similar)?

4. Is 'g' defined in a grammatical correct manner, or does composition have to be defined differently? (Remember that the functions to be composed is provided in a set as an argument.)

5. Finally, should this problem preferably be solved differently?

It will be interesting to see if anyone has something here. Also, thanks for taking the time to read this regardless of your contribution.

Have a great day!

Interesting that there are no replies. Is there something I should specify more clear, or other things that should be sorted out?

Have a good morning!