# 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

### ##plugins.generic.usageStats.downloads##

##plugins.generic.usageStats.noStats##

## ##plugins.themes.bootstrap3.article.details##

How to Cite
Shalack V. I. Weak consequence relation between $\lambda$-terms // Logicheskie Issledovaniya / Logical Investigations. 2018. VOL. 24. № 2. C. 151-157.
Issue
Section
Papers

## References

Барендрегт Х. Ламбда-исчисление. Его синтаксис и семантика. М.: Мир, 1985. 606 с.
Hindley R.J., Seldin P. Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, 2008. 345 p.