cn ` cn
n`n s`s
n ` n n, n\n ` s
n, (n\s)/n, n ` s
n, (n\s)/n ` s/n
- [\L]
[/L]
[/R] —
s`s
n, (n\s)/n, (s/n)\s ` s
(n\s)/n, (s/n)\s ` n\s
— [\L]
[\R] —
s`s
s/(n\s), (n\s)/n, (s/n)\s ` s
[/L]
cn ` cn (s/(n\s))/cn, cn, (n\s)/n, (s/n)\s ` s
[/L]
(s/(n\s))/cn, cn, (n\s)/n, ((s/n)\s)/cn, cn ` s
[/L]
Figure 1: Proof for ‘a man adores a woman’
3 From Lambek Proofs to Semantical Recipes
Proof theory teaches us that there is a close correspondence between proofs
and lambda terms. The lambda term which corresponds to a given proof can
be obtained with the help of the so-called Curry-Howard correspondence. Van
Benthem [1986] observed that the lambda term that we get in this way also
gives us a correspondence between Lambek proofs on the one hand and the
intended meanings of the resulting expressions on the other. In the present
exposition of the Curry-Howard-Van Benthem correspondence I shall follow
the set-up and also the notational conventions of Hendriks [1993]. For more
explanation, the reader is referred to this work, to Van Benthem [1986, 1988,
1991] and to Moortgat [1988].
The idea behind the correspondence is that we match each rule in the
Lambek calculus with a corresponding semantic rule and that, for each proof,
we build an isomorphic tree of semantic sequents, which we define as expres-
sions T0 ` γ, where T0 is a sequence of variables and γ is a lambda term with
exactly the variables in T0 free. The semantic rules that are to match the
rules of the Lambek calculus above are as follows. (The term γ[u := w (β)]
is meant to denote the result of substituting w(β) for u in γ.)
More intriguing information
1. Demographic Features, Beliefs And Socio-Psychological Impact Of Acne Vulgaris Among Its Sufferers In Two Towns In Nigeria2. IMPACTS OF EPA DAIRY WASTE REGULATIONS ON FARM PROFITABILITY
3. The name is absent
4. Innovation Policy and the Economy, Volume 11
5. AN ECONOMIC EVALUATION OF COTTON AND PEANUT RESEARCH IN SOUTHEASTERN UNITED STATES
6. The name is absent
7. Update to a program for saving a model fit as a dataset
8. The name is absent
9. Großhandel: Steigende Umsätze und schwungvolle Investitionsdynamik
10. The InnoRegio-program: a new way to promote regional innovation networks - empirical results of the complementary research -