Because it is the simplest thing we have, and has a pretty straightforward self-interpreter.
It feels like you need a lot more metamathematics to deal with typed lambda calculus than with untyped one, and types are something that comes without a justification.
Anyway, the idea is, if you have a language, you can think of source code written in the language as a giant lambda term, where you have all lambdas upfront and only composition in the body. A tree of symbols to be composed, essentially. And then to interpret this source code in a language, you supply definitions of the language's primitives as arguments to the source code term.
Now if your language is typed, the primitives need to be chosen in such a way, so that the interpreted term (the source code applied to language primitives) fails to normalize if the program is not typed correctly.
You can then have a correspondence between the primitives of the typed language that typecheck and simpler set of primitives of the same language used purely for computation, used under the assumption that the program typechecks. This correspondence "defines" the typing mechanism of your language (in untyped lambda terms).
Yes, that's deliberate though. (I will call these "concrete" terms, because they lack abstraction in the body, but I am looking for a good name. In fact, no universal one-point basis can be expressed as a single term like that, you need a composition of two; the concrete property is not preserved in composition, although it might be preserved in weaker bases than S,K, such as B,C,K - kind of affine logic.)
Anyway, the reason I am interested in concrete terms is I want to define typing judgements in ULC somehow. (In CoC, all mathematical questions can be rephrased as is there an object of given type T, and you need to be able to formalize questions somehow to formalize metamathematics.)
An obvious definition of typing judgement in ULC would be: term x is of type B in a typed language A (both A and B are given terms) iff there exists a term x that satisfies Ax = B (the equality is judgemental after beta-normalization).
However, this definition doesn't work, because a general term x can just disregard A and return B directly. But - I think if we restrict x to be a concrete term in the above definition (possibly with a given number of upfront lambdas - not sure if that is required), then I think we can make the definition to work.
I also suspect concrete terms can be sort of "deconstructed from the outside". In general, we cannot resolve equality of terms, but I suspect that concrete terms can be analyzed (and quoted) within ULC.
One thing I realized about your CoC implementation - I think you embed CoC into ULC in an indirect way, working with CoC terms in a quoted way. And that's fine, but what I want is to have CoC in ULC directly, i.e. have a base set of ULC terms for the primitives of CoC language. But that also can be thought of as the CoC interpreter being restricted to apply on concrete terms, giving them meaning by substituting the base inside.
In other words, concrete terms are kind of "inside view" of quoting. (Maybe we should call them "data terms", because they effectively carry only data and no executable payload.) Having the concept of concrete terms in the ULC metalanguage can also help to define interaction to the external world, that you only accept data not executables, something that you kinda do through the "monadic" interface. (You need to "remember" that a term only accepts quoted data, it cannot be made explicit in ULC language. The advantage of concrete terms is they are independent on your choice of quoting operator.)
Anyway, I am not sure if I am making sense, I am trying to grapple with this myself, so it's OK if you don't think concrete terms are a useful concept.
No, that equation can be created as a special case from equation TAx = B (where Txy = yx is a transposition combinator).
> Not if you require x to be strict, i.e. it must use its argument.
I am not sure it would generally help but maybe you mean it only in case of equations xA=B (not Ax=B as I suggested). I also think this strictness condition would be too limiting.
In equation Ax=B, we can take A of the form R_n A_1 .. A_n, where R_n reduces Ax to x A_1 .. A_n (R_n rotates x in front of n arguments).
So if x is concrete and takes n arguments, we can think of it as "text" (parenthesised expression) in symbols that are to be interpreted as A_1, .. A_n. Requiring that every possible symbol is used in a language text fragment is a weird condition, which doesn't make much sense to me.
In any case, my definition of typing judgment then allows to put a chosen condition on a text composed from chosen symbols, which is quite powerful and can be used to e.g. determine whether a quoted expression is valid. And arguably it is a very natural definition in the context of ULC. (I read to Mock a Mockingbird 30 years ago - in partial Slovak translation - and most problems there could be formulated as the Ax=B equation for x being a concrete term.)
It feels like you need a lot more metamathematics to deal with typed lambda calculus than with untyped one, and types are something that comes without a justification.
Anyway, the idea is, if you have a language, you can think of source code written in the language as a giant lambda term, where you have all lambdas upfront and only composition in the body. A tree of symbols to be composed, essentially. And then to interpret this source code in a language, you supply definitions of the language's primitives as arguments to the source code term.
Now if your language is typed, the primitives need to be chosen in such a way, so that the interpreted term (the source code applied to language primitives) fails to normalize if the program is not typed correctly.
You can then have a correspondence between the primitives of the typed language that typecheck and simpler set of primitives of the same language used purely for computation, used under the assumption that the program typechecks. This correspondence "defines" the typing mechanism of your language (in untyped lambda terms).