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)
| Autoři | |
|---|---|
| Rok publikování | 2016 |
| Druh | Další prezentace na konferencích |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | 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. |
| Související projekty: |