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)

Logo poskytovatele
Autoři

PEZLAR Ivo

Rok publikování 2016
Druh Další prezentace na konferencích
Fakulta / Pracoviště MU

Filozofická fakulta

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.