A problem in the interpretation of CIL

What is, linguistically,  $[B([A(x)])]_x$, that is,  $comb_{(1)} B^{(1)} A^{(1)}$ ? Prima facie the only real linguistic interpretation we can think of involves propositional attitudes. $[B([A(x)])]_x$ is the property that an $a$ satisfies when it is the case that $[B([A(a)])]$. We could read it as: the property of  $[A(x)]$ being $B$. But could this be written $\lambda x. [B([A(x)])]$ or $\lambda x. comb_{(0)}Bcomb_{(0)}Ax$ ? 

Consider the following system called $\lambda$CIL.  As in CIL each term that is not a variable has a unique sort.  For each sort we have a list of primitive terms. We have a set of variables which are terms. Given a sequence  $s$ of  $m$ distinct integers for $m \leq n$, $m$ terms $T_i$ and a term $T$ of sort $n$ we have that $comb_s T T_1...T_m$ is of sort $n- m$.  Given a term $T$ of sort $n$ we have that $\lambda x. T$ is a term of sort $n+1$. CIL can be represented in $\lambda$CIL and vice-versa. But $\lambda$CIL is not suitable for CIL models.

CIL must be extended to be able to talk about its own syntax. Expressions of the form 'an A is a B' or 'A = B' convey information or might be even seen as definitions. If A and B are both constants then A = B conveys the meaning that the expressions 'A' and 'B' have the same meaning. Given a CIL term T we can write T' for the term whose sense is the expression T itself (not the sense of T). This may seem odd. But consider the definite description 'the letter in the Roman alphabet after 'a''. The denotation is contained in some way in this sense.