1
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • $\begingroup$ What is higher order rewriting? $\endgroup$ Commented Aug 24, 2018 at 21:02
  • $\begingroup$ It is rewriting with rules that contain bound variables. Teresa Rewriting book has chapter 11 about higher-order rewriting. $\endgroup$ Commented Aug 24, 2018 at 21:09
  • 1
    $\begingroup$ All of your terms are closed though. Which part from Andrej's answer doesn't meet your need? Your source and target terms are definitionally equal. I do not see much complexity. $\endgroup$ Commented Aug 24, 2018 at 21:12
  • $\begingroup$ I am suspicious about possibility to use re-currying in the general case. In this case it is simple, because 'is' uses e and e->t functions and they should be reordered only when moving to 'IS'. But, generally, the more complex re-currying may happen that can require to re-curry inner functions and I doubt that that is possible. $\endgroup$ Commented Aug 24, 2018 at 21:21
  • 1
    $\begingroup$ You should explain that situation in details. I still agree with Andrej. As long as it's about shuffling the order and form of syntax, it's just a matter of cutting and uncurrying. $\endgroup$ Commented Aug 24, 2018 at 21:33

1 Answer 1

Reset to default
4
$\begingroup$

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).

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.