Zkoumání struktury termů v lambda kalkulu na základě jejich typů
| Název práce v češtině: | Zkoumání struktury termů v lambda kalkulu na základě jejich typů |
|---|---|
| Název v anglickém jazyce: | Examining the structure of terms in lambda calculus based on their type |
| Klíčová slova: | lambda kalkul, teorie typů, závislostní typy, strukturální indukce, induktivní typy |
| Klíčová slova anglicky: | lambda calculus, type theory, dependent types, structural induction, inductive types |
| Akademický rok vypsání: | 2019/2020 |
| Typ práce: | diplomová práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra teoretické informatiky a matematické logiky (32-KTIML) |
| Vedoucí / školitel: | RNDr. Jan Hric |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 06.08.2020 |
| Datum zadání: | 07.08.2020 |
| Datum potvrzení stud. oddělením: | 12.08.2020 |
| Zásady pro vypracování |
| Lambda calculus is a very simple term rewriting system with a wide range of use in informatics and mathematics. It is a universal system of computations (an alternative to Turing machines), but it has also found its way into logic and theorem proving thanks to Curry-Howard isomorphism which states that every system of logic corresponds to a system of computations. The basic, untyped form of lambda calculus cannot be used for theorem proving because it can express unbounded computations leading to paradoxes. To solve this, types can be added. With a suitable, consistent type system, a type will express a theorem and a term of that type will be a proof of that theorem. This principle has already been used to develop type theories as foundations of mathematics (Martin-Löf's type theory, homotopy type theory) and automated proof assistants (Coq, Agda).
The beauty of untyped lambda calculus lies in the fact that everything is a function and functions are used to create more complex data structures (numbers, pairs, lists, trees). In typed lambda calculus, this principle is thrown away even though the constructions have straightforward types because nowadays type systems do not allow induction to be performed on function terms. Instead, they introduce 'inductive types' (similar to algebraic data types) which are specified with a fixed set of cases (called constructors in functional programming) for the type (e.g. zero and successor for natural numbers) and then induction can be used. These type systems do not take any advantage of the fact that a type of a function restricts the form of terms satisfying this type. In this thesis, a goal is to explore how types restrict/guide the structure of terms which satisfy them, at least for some types. Our results could improve inductive reasoning, particularly structural induction on lambda terms and integrate it into a type system. As a possible application, inductive types available in current type systems could be represented and/or replaced using this approach. Generally, it can open doors to new type construction methods and theorem proving techniques. Although the core work is theoretical, it should be applied practically to produce a working proof-of-concept implementation. |
| Seznam odborné literatury |
| Hendrik Pieter Barendregt, Wil Dekkers, Richard Statman, Lambda Calculus with Types. Perspectives in logic, Cambridge University Press 2013, ISBN 978-0-521-76614-2, pp. 833
Peter Dybjer, Erik Palmgren, Intuitionistic Type Theory. The Stanford Encyclopedia of Philosophy (Summer 2020 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/sum2020/entries/type-theory-intuitionistic/ Daniel P. Friedman, David Thrane Christiansen, The Little Typer. The MIT Press, 2018 Amin Timany, Matthieu Sozeau, Cumulative Inductive Types In Coq. 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, LIPIcs 108, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2018, ISBN 978-3-95977-077-4, pp. 29:1-29:16 Philip Wadler, Theorems for free! Functional Programmimg Languages and Computer Architecture (FPCA 1989), ACM Press, 1989, pp. 347-359 |