5
$\begingroup$

Natural language semantics (in computational linguistics) uses lambda terms for expressing the semantics of natural language sentences. There is vast literature about combinatorial categorial grammars and lambda semantics of natural language, e.g. tutorial about framework http://yoavartzi.com/tutorial/

The question is - if lambda calculus can be used to represent the meaning of the natural language text, then can we use lambda calculus for the universal representation of knowledge? Why there are so few results in this direction? Or maybe there are efforts to bridge the meaning as expressed in lambda calculus with some of the common knowledge representation approaches?

Maybe (extended) Curry-Howard isomorphism between lambda calculus and logical/deductive systems can be used to translate the semantics in terms of lambda calculus into knowledge in terms of logical expressions, e.g., maybe translation to description logics and action logics is possible?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ C-H is between types and propositions (Propositional Logic). To represent knowledge you need predicates/relations and quantification (Predicate Logic). Which is beyond C-H: I already asked cs.stackexchange.com/questions/77888/…. Combinator/Categorial grammars are about syntax, not semantics. But if you want a unifying framework, that could be Montague grammars en.m.wikipedia.org/wiki/Montague_grammar. In particular, Max Cresswell uses lambda calculus en.m.wikipedia.org/wiki/Max_Cresswell. $\endgroup$
    – AntC
    Commented Aug 10, 2017 at 12:43
  • $\begingroup$ "The Curry-Howard isomorphism states an amazing correspondence betweensystems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed λ-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types" - this citation is from the preface of "Lectures on the Curry-Howard Isomorphism" by Sørensen and Urzyczyn. Google can find several PDF copies of this book. So, that is fine. So - my question is valid indeed.. $\endgroup$
    – TomR
    Commented Aug 10, 2017 at 19:05

1 Answer 1

Reset to default
5
+50
$\begingroup$

The λ-calculus was invented to be a logic and foundation of mathematics (1-4). The most well-known logic to use λ-calculus for formulae (as opposed to proofs in the Curry-Howard approach) is HOL (= Higher-Order Logic). The most well-developed implementation of HOL is Isabelle/HOL (5). To the extent that you believe logic can represent knowledge, you can use HOL to do that, hence λ-calculus.

There is a third approach to using λ-calculus as logic: higher-order Prolog (aka λProlog) (6), which -- like Prolog -- is based proof search, but in HOL.

The relationship between the three approaches (HOL, Curry-Howard and λProlog) is not well-understood.

1. A. Church, A Formulation of the Simple Theory of Types.

2. P. B. Andrews, Churchs Type Theory.

3. F. Cardone, J. R. Hindley, History of Lambda-calculus and Combinatory Logic.

4. J. B. Rosser, Highlights of the history of the lambda-calculus.

5. T. Nipkow L. C. Paulson, M. Wenzel, A Proof Assistant for Higher-Order Logic.

6. D. Miller, G. Nadathur, P. Pfenning, A. Scedrov, Uniform Proofs As A Foundation For Logic Programming.

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.

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