Relative clauses and lambda calculus

I've been thinking that relative clauses are just like functions in lambda calculus, and that abstraction could be eliminated using the S, K and I combinators. I thought about this when reading about the obfuscated programming language Unlambda:
http://www.eleves.ens.fr:8080/home/madore/programs/unlambda/unlambda.html

Suppose we have a language where roots are isolated and the only thing one can do is "applying" a root to another root. The functor would be the modifier and the arguments modified.

BNF syntax

Syntax would be quite simple (in a kind of BNF):

Where ` is the apply operator. ` A B reads "apply A to B". And every other construction would be delegated on semantics.

Some simple examples

Let's work with English words as roots for some examples (I'll also assume English semantics, but it is not the point):

Intransitive verbs are just applied to nouns:

` write man
the man writes

Adjectives are simply intransitive verbs (just like in many natural languages):

` white book
the book is white = white book

Of course, application is recursive:

` write ` tall ` red man
the tall red man writes

Adverbs could be applied to adjectives or verbs:

` ` quickly write ` ` amazingly tall man
the amazingly tall man writes quickly

Transitive verbs are (in currying fashion) verbs that when applied to a nominal construction (the object, maybe?) yields an intransitive verb that, when applied to a second nominal construction (the subject), yields the expected result:

` ` write* book man
the man writes a book

Where: ` write* book corresponds to the verb "to write-a-book".

Notice that in the language, intransitive write and transitive write* should be different words (probably regularly related).

Oblique constructions should be applied to the verb, too:

` ` ` in sky fly plane
the plane flies in the sky

Many ambiguities dissapear:

` ` see ` ` with telescope man I
I see [a man with a telescope]

` ` ` ` with telescope see man I
I see [a man] with a telescope

` ` hate ` ` and dance ` eat cheese I
I hate [dancing and eating cheese]

` ` ` and ` hate dance ` eat cheese I
I hate dancing and I eat cheese

Now let's analyse relative clauses. Just like adjectives can be interpreted like intransitive verbs or adjectives, when translated:

We could do the same with verbs:

Non-trivial relative clauses

When the order is the expected, there are no problems. But what if we want to express, say:

We cannot say:

And neither:

Lambda notation

We need more expressive constructions. Adopting lambda notation for functions (where \ pretends to be the ASCII version of a greek lowercase lambda):

Is a construction that, when applied to an argument x, means "the man writes x".

For instance:

Therefore:

Notice that if we reduce it:

It yields the previously discarded construction. Expressions with lambdas are not necessarily equivalent when reduced. Here, lambdas are precisely used to show that the modified root is "book" and not "man".

We could invent a way of directly translating lambda expressions into our conlang.

But there is an ugly problem: the name x. In math, its said of x that it is a mute variable, as changing its name does not change the meaning of the expression.

Fortunately, this problem has already been solved with the S, K and I combinators.

Definition of the S, K and I combinators

I is the identity function:

K is the constant function generator:

And S is the substituted application function:

Lambda elimination

By induction, it's not hard to prove that any lambda expression can be reduced to an expression using these combinators, and without any mute variable.

A lambda expression (\ x : e) falls into one of these three cases:

1. e is x

   In this case, (\ x : e) = (\ x : x) , which is precisely I!!

2. e is a constant, or another variable not being x

   In this case, (\ x : e) = (\ x : a) , which is ` K a

   Note that: ` (\ x : a) b = a = ` ` K a b


3. e is the application ` f g:

   (\ x : e) = (\ x : ` f g) , which is ` ` S (\ x : f) (\ x : g) (and then the we eliminate the lambda in the inner expressions f and g which, by induction, are simpler and we already know how to reduce. Note that:
` (\ x : ` f g) b = ` ` (\ x : f) b ` (\x : g) b = ` ` ` S (\x : f) (\x : g) b

Rules for eliminating abstraction

A rule for mechanically eliminating abstraction in lambda expressions (\ x : e):

Reading e from left to right, replace:

If more than one lambda need to be eliminated, start with the innermost ones first.

Examples

Now let's eliminate the abstraction from:

Conclusion

The power of lambda expressions guarantees that every possible relative clause is expressable in this language, and that no ambiguities can appear in nested clauses.

An example of a relative clause impossible in English from the Language Construction Kit:

(Notice I write the first person pronoun as "i" to avoid confusion with "I", the identity function! <POSS> is a root for possessive, where ` ` <POSS> X Y = X's Y).

Which is a bit quite long. Some tricks could be used to make it shorter. There's much more about it in the Unlambda reference.

These kilometric expressions make me believe this is probably violating a language universal, in the sense that it is counter-intuitive. Anyway, at least for me, it is an interesting theoretical exercise.

To create a real conlang, the apply operator should be grammaticalized somehow (as an inflection, syntactically, etc.). I leave the rest as an exercise to the conlang world.