A Few Notes on Lambda-Computation and TIL-Construction (21st Conference Applications of Logic in Philosophy and the Foundations of Mathematics, Szklarska Poręba, 10. 5. 2016)



Year of publication 2016
Type Appeared in Conference without Proceedings
MU Faculty or unit

Faculty of Arts

Description Lambda calculus (abbr. LC) originally developed by (Church, 1932) can be regarded as the most universal tool for expressing computations (Turing, 1937). Its fundamental computation rule, so called beta-reduction, is defined in terms of substitution and it embodies the idea of function application. Consequently, each application of beta-reduction rule can be regarded as a single computational step. There is, however, at least one formal system utilizing lambda calculus in which these correspondences (roughly put, computational step = beta-reduction = function application) do not hold. It is called transparent intensional logic (abbr. TIL) and it was developed by (Tichý, 1988). I will, however, focus on one of its later variants found in (Duží, Jespersen, Materna, 2010). In the present talk I will examine this deviation from standard lambda calculus and explore the outcomes it entails for the corresponding system.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.