Weak consequence relation between $ \lambda $-terms

Abstract

The language of the $\lambda$-calculus has many applications for solving different problems in logic, information technology, linguistics and artificial intelligence. The $ \lambda$-calculus is based on the basic relation between terms, which is called $ \beta $-conversion. In the presented report, we formulate a weaker relation between the $ \lambda $-terms, which makes it possible to establish more subtle connections between logic and $ \lambda$-calculus. The basic idea is that when we assign a type $ \alpha $ to a term $ X $ relative to the context $ \varGamma $, which is written in the form $ \varGamma \vdash X:\alpha $, the concept of context plays a role analogous to the concept of a model in logic. If in logic the expression $ M \vDash A $ means that the formula $ A $ is true in the model $ M $, then in the $ \lambda$-calculus with types the expression $ \varGamma \vdash X:\alpha $ means that in the context $ \varGamma $ the term $ X $ is assigned the type $ \alpha $, and this term has a value that can be computed. In logic, the relation of logical consequence between the formulas $ A $ and $ B $ is defined as $ A\vDash B \Leftrightarrow \forall M(M\vDash A \Rightarrow M\vDash B) $. If we transfer this scheme to the $ \lambda $-calculus, then the $ \lambda $-consequence relation between terms can be defined as $ X \vDash _{\lambda} Y \Leftrightarrow \forall \varGamma \in Ctx [\exists\alpha(\varGamma \vdash X:\alpha) \Rightarrow \exists\beta(\varGamma \vdash Y:\beta)] $. The meaning of this relation is that in every context in which we can assign some type to the $ X $, we can also assign some type to the term $ Y $. In other words, if the function represented by the term $ X $ is computable, then the function represented by the term $ Y $ is also computable. The $ \lambda $-consequence between terms relation has many properties analogous to the classical logical consequence relation between formulas, as well as a number of new properties, characteristic for the $ \lambda$-calculus with types. DOI: 10.21146/2074-1472-2018-24-2-151-157