I am reading Categorial Grammar: Logical Syntax, Semantics, and Processing by Glyn Morrill and I am stuck with the Fig. 3.9: enter image description here

Can someone explain this set of formulas and |.| function specifically?

This figure displays the definition of the |.| function that maps some proof (of some formula) in Lambek calculus (as fragement of intuitionistic logic) into lambda-term (by Curry-Howard correspondence there is correspondence between proof in some logic and terms in lambda calculus). I understand Lambek calculus and lambda calculus but I can not understand this picture? It is said in this book, tht |.| function is applied to proof, but this picture say something different - this function is applied to proof rules, that is completely different structure. What does small indices mu(ni, psi) and so on mean?

This was very good book up to this chapter, I am completely lost.


1 Answer 1


What constitutes a proof in a system like this is a derivation which is a tree of rule applications. The above translation function is defined by (structural) recursion over that tree. Note, this is why it labels the premises in the rules with $\delta$. This is intended to be mnemonic for "derivation".

I'm guessing but $\mu$ and $\nu$ appear to need to be sequences of lambda terms, while $\phi$ is a specific lambda term (or, equivalently, a single element sequence of lambda terms). $\Gamma$ is a sequence of formulas, and $\mu$ has a lambda term for each element of that sequence. Constructs like $x,\mu$ correspond to sequence extension, extending the sequence $\mu$ with the (particular) lambda term $x$ on the left, symmetrically for $\mu,x$. The parenthesis notation, e.g. $\Gamma(C)$ and $\mu(\dots)$ correspond to (consistently) operating on an element at an arbitrary location in the sequence.

So, for example, an instance of the $\bullet R$ case would look like: $$\left|\cfrac{\cfrac{\delta}{X,A,B,Y,Z\Rightarrow W}}{{X,A\bullet B,Y,Z\Rightarrow W}}\right|_{t_X,t_{AB},t_Y,t_Z} = \left|\cfrac{\delta}{X,A,B,Y,Z\Rightarrow W}\right|_{t_X,\pi_1(t_{AB}),\pi_2(t_{AB}),t_Y,t_Z}$$

A translation of a complete derivation would look like: $$\begin{align} \left|\cfrac{\cfrac{A\Rightarrow A \qquad B \Rightarrow B}{A,B\Rightarrow A\bullet B}}{\cfrac{A\Rightarrow (A\bullet B)/B}{\Rightarrow ((A\bullet B)/B)/A}}\right| & = \lambda a\left|\cfrac{\cfrac{A\Rightarrow A \qquad B \Rightarrow B}{A,B\Rightarrow A\bullet B}}{A\Rightarrow (A\bullet B)/B}\right|_a \\ & = \lambda a\lambda b\left|\cfrac{A\Rightarrow A \qquad B \Rightarrow B}{A,B\Rightarrow A\bullet B}\right|_{a,b} \\ & = \lambda a\lambda b(\left|A\Rightarrow A\right|_a, \left|B \Rightarrow B\right|_b) \\ & = \lambda a\lambda b(a, b) \end{align}$$


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.