Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I have expressions (type of a function) like e.g.

$$f:(A\to B)\to C \to (D\to E)\to F.$$

(Where I understand $A\to B\to C$ as $A\to (B\to C)$, in case that is relevant.)

There might be information associated with each symbol/type "$A,B,...$" as well as with each of the arrows "$\to$". Given the expression above, I would like to refer to these symbols, but not by stating the symbol but in terms of $f$. Like for example I might want to say "$E$ is $\mathbb{R}$." and would naively express this like "$f_{9}$ is $\mathbb{R}$." where I just made up the convention that $f_i$ denotes the $i^{\text{th}}$ symbol in the type of $f$. I could equally well refer to the two objects "arrow-symbol" and "non-arrow-symbol" seperately, so that in this case $E$ would be the $5^{\text{th}}$ non-arrow symbol. Or I could take into account that e.g. "$(A\to B)\to C$" is totally differently "stacked" than "$A\to (B\to C)$" and hence use an enumeration which climbs down that syntactic tree.

Is there a standard or canonical way to refer to the items of an expression (logic, type, any syntactic expression really)? More generally one might ask if there is some canonical enumaration principle for trees.

I'm concerend with types of functions here, but the question can be understood as a more general reference request for standard notation.

I also don't know about normal forms of types, which might be relevant to make the enumeration more robust in case there are more ways to do it (robust in that the enumeration would not by dependend of the particular way the type is stated).

share|improve this question
    
It might be worth looking at De Bruijn index and De Bruijn notation, then refer to particular type symbols, for example, via the stacked indexes of the corresponding lambda term. –  dtldarek Feb 5 '13 at 13:03
    
As for canonical enumerations, you can go with a pre-, in- or post-order. Also any algebraic type such as $T[\alpha] = \alpha + T^2[\alpha]$ would give you some enumeration. Finally, you can refer to nodes by a path from root, e.g. LRRLRL or something similar. –  dtldarek Feb 5 '13 at 13:07
    
@dtldarek: The De Bruijin seems to be just a rewriting which gives me no obvious way of refering to a particular symbold within the expression. I don't understand the second post, except for the LRRLRL-thing. –  NikolajK Feb 5 '13 at 13:22
    
Those are orderings derived from DFS tree. The given algebraic type is a type of a tree, by numbering the operators/constructors you get some enumeration method (this is usually similar to 'path from root' method, but has different motivation and might be easier or harder to deal with, depending on the context). –  dtldarek Feb 5 '13 at 13:29

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.