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
is has type
boss has type
(e->t). The the full sentence is translated as the lambda expression:
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:
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
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->(e->t)->t? Are there some apparatus/algorithms/methods how can I express function
isvia the function
ISand how can I transform terms involving
isinto terms that does not contain
isand 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 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? 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?