Praca doktorska
Miniatura
Pliki
0000-DR-8122-praca.pdf1.01 MB
Licencja
FairUseKorzystanie z tego materiału możliwe jest zgodnie z właściwymi przepisami o dozwolonym użytku lub o innych wyjątkach przewidzianych w przepisach prawa. Korzystanie w szerszym zakresie wymaga uzyskania zgody uprawnionego.
 

A Functional Programming Language for Sets with Atoms

Uproszczony widok
dc.abstract.enThis thesis describes a functional programming language Nλ that operates on infinite structures using sets with atoms. For relational structures satisfying certain condi tions, hereditarily orbit-finite sets with atoms admit a finite representation based on first-order logic formulas. Thanks to this property, the presented language enables the implementation of programs that perform calculations on infinite objects, such as graphs or automata. Such infinite objects are accessed in ways similar to their finite counterparts. Therefore, many algorithms operating on finite structures can be naturally transported to the world of infinite objects. The Nλ language is presented as an extension of the simply typed lambda cal culus. The syntax of the language and its denotational and operational semantics are described. Each language term is assigned a type using appropriate typing rules. Additionally, denotational semantics assign meaning to terms in the form of mathematical objects. In this case, they are atoms, truth values, sets, and func tions. Operational semantics, through a list of reduction rules, defines the actual computational model of the language. The language has several expected properties that have been proven. It is shown that the reduction rules preserve the type (subject reduction) and the meaning (denotation) of the term. Additionally, the language has Church-Rosser property and strong normalization. The above properties have been proven for a core version of the language. To be considered as a full-fledged functional programming language, Nλ must additionally have constructs present in modern, commonly used programming languages. There fore, possible extensions of the core version are indicated. The possibility of adding recursion, polymorphism, or algebraic types is discussed. In addition to the theoretical description of the Nλ language, its implementa tion in Haskell was also provided. As a result, the language user, apart from the implementation of programs that perform calculations on infinite data structures, can use all Haskell functionalities. To solve and simplify first-order logic formulas, the language implementation integrates with an external SMT solver. Some inter esting applications of the language for algorithms on infinite graphs and automata are discussed.
dc.abstract.plNiniejsza rozprawa przedstawia funkcyjny język programowania Nλ operujący na strukturach nieskończonych opartych na zbiorach z atomami. Dla struktur relacyjnych spełniających określone warunki, zbiory z atomami, które są dziedzicznie skończenie orbitowe, posiadają skończoną reprezentację bazującą na formułach pierwszego rzędu. Przedstawiony język, wykorzystując tę własność, umożliwia implementację programów działających na obiektach nieskończonych takich jak grafy lub automaty. Takie nieskończone obiekty są dostępne za pomocą analogicznych funkcji i interfejsów jak ich skończone odpowiedniki. Dlatego wiele algorytmów działających na konstrukcjach skończonych może być naturalnie wykorzystanych w świecie struktur nieskończonych. Język Nλ został przedstawiony jako rozszerzenie rachunku lambda z typami prostymi. Opisana została jego składnia, semantyka denotacyjna oraz semantyka operacyjna. Każdy term języka ma przypisany typ za pomocą odpowiednich zasad typowania. Semantyka denotacyjna dodatkowo przypisuje termom ich znaczenie w postaci obiektów matematycznych. W tym wypadku są to atomy, wartości logiczne, zbiory oraz funkcje. Semantyka operacyjna poprzez listę reguł redukcyjnych przedstawia właściwy model obliczeniowy na strukturach nieskończonych. Tak opisany język ma oczekiwane własności, które zostały udowodnione. Chodzi o zachowywanie przez reguły redukcyjne typów i denotacji (znaczenia) termów, własność Churcha-Rossera oraz silną normalizację. Powyższe własności zostały wykazane dla podstawowej wersji języka. Jednak aby język Nλ mógł być rozpatrywany jako pełnoprawny język programowania, musi zostać rozszerzony o konstrukcje obecne we współczesnych, powszechnie używanych językach programowania. Dlatego wskazane zostały możliwe rozszerzenia podstawowej wersji o takie konstrukcje jak rekurencja, polimorfizm czy typy algebraiczne. Poza teoretycznym opisem języka Nλ została również dostarczona jego implementacja w języku Haskell. Dzięki temu użytkownik języka poza implementacją programów wykonujących obliczenia na nieskończonych strukturach danych może korzystać ze wszystkich funkcjonalności Haskella. W celu sprawdzania prawdziwości oraz upraszczania formuł logicznych pierwszego rzędu implementacja języka integruje się z zewnętrznym narzędziem w tym się specjalizującym (SMT solver). Rozprawa opisuje także ciekawsze zastosowania języka do algorytmów na grafach i automatach nieskończonych.
dc.affiliation.departmentWydział Matematyki, Informatyki i Mechaniki
dc.contributor.authorSzynwelski, Michał
dc.date.accessioned2022-10-21T07:21:38Z
dc.date.available2022-10-21T07:21:38Z
dc.date.defence2022-12-08
dc.date.issued2022-10-21
dc.description.additionalLink archiwalny https://depotuw.ceon.pl/handle/item/4336
dc.description.promoterKlin, Bartosz
dc.identifier.urihttps://repozytorium.uw.edu.pl//handle/item/4336
dc.language.isoen
dc.rightsFairUse
dc.subject.ensatisfiability modulo theories
dc.subject.enHaskell
dc.subject.enfunctional programming
dc.subject.enlanguage semantics
dc.subject.enlambda calculus
dc.subject.endefinable sets
dc.subject.ensets with atoms
dc.subject.plteorie modulo spełnialności
dc.subject.plHaskell
dc.subject.plprogramowanie funkcyjne
dc.subject.plsemantyka języka
dc.subject.plrachunek lambda
dc.subject.plzbiory nominalne
dc.subject.plzbiory z atomami
dc.titleA Functional Programming Language for Sets with Atoms
dc.title.alternativeFunkcyjny język programowania dla zbiorów z atomami
dc.typeDoctoralThesis
dspace.entity.typePublication