How to transform lambda function to multi-argument lambda function and how to rewrite or approximate terms?

Question

I am trying to do the formal semantics (Montague grammar, abstract categorial grammar) of natural language and encode the sentence John is boss. The type system has to primitive types - e for entity and t for Boolean type. John has type e, is has type (e->t)->(e->t) and boss has type (e->t). The the full sentence is translated as the lambda expression:

(is(boss))(John): t

I don't like the chaining of functional application and more intuitive presentation could be by introducing new function IS of type (e, (e->t)) and hence the expression could become:

IS(John, boss): t

And by moving boss from the argument the function index we can arrive to the standard predicate expression with new predicate-function:

IS_BOSS(John): t

I have two questions regarding this example:

• Does standard lambda calculus have multi-argument functions? As I guess that these calculus have such function by currying and hence the real type if IS is e->(e->t)->t. So, this part seems to be already answered.
• And now is the main question - does lambda caluclus allow do function transformation - e.g. is there some operation which transforms is:(e->t)->(e->t) into IS:e->(e->t)->t? Are there some apparatus/algorithms/methods how can I express function is via the function IS and how can I transform terms involving is into terms that does not contain is and that contains IS? Are there some rewriting apparatus available for this in lambda calculus?

This question is inspired by the book https://www.amazon.co.uk/Elements-Formal-Semantics-Introduction-Mathematical/dp/0748640436 and uses notions and notation from this book.

Important note. I do not expect that is and IS are identical functions (but I would be glad to consider the case when some kind of identity is assumed as well). I expect that is is more general function (that is used for the processing of the raw text) and that I try to express it using more specialised function IS (which can convey more specific meaning, e.g. borrowing from pragmatics (branch of lingustics): I can analyse context and determine that in this context such detalization is desirable). Maybe rewrite operation should be used but maybe some other tools should be used - simply - how to transform term using these functions? Maybe I am just trying to approximate function is with function IS (of different type!) and is-terms with IS-terms? Are there such notions, theories?

Maybe I should look to higher-order rewriting of lambda terms? Is there example available how my terms could be rewritten inside such framework?

Answer 1

You are looking for currying and uncurrying which transform functions of type $A \times B \to C$ to functions of type $A \to (B \to C)$, and vice versa. Currying takes IS to is, while uncurrying takes is to IS. This is a standard and very basic technique in $\lambda$-calculus. There are many manifestations of currying and uncurrying, for instance in arithmetic it is the identity $c^{a \cdot b} = (c ^ b) ^ a$.

It is largely a matter of taste how you write multi-argument functions. The uncurried form $A \to (B \to C$ has the advantage that you can apply the function only to the first argument. In your case is boss is a useful concept which is expressible very neatly. With the other function you have to write λ x . IS (boss, x).

Note however that sometimes people do not include product types $A \times B$ in their versions of $\lambda$-calculus, in which case of course currying is unavailable (but nothing much is lost).