Στη διπλωματική αυτή αναπτύσσουμε μια νέα, μη-κατασκευαστική απόδειξη του
θεωρήματος σταθερού σημείου, που προτάθηκε από τους Α. Χαραλαμπίδη, Γ.
Χατζηαγάπη, και Π. Ροντογιάννη (LICS20). Το θεώρημα αυτό αφορά στην ύπαρξη
ελάχιστου σταθερού σημείου μιας κλάσης συναρτήσεων που διαθέτουν ένα
περιορισμένο είδος μονοτονικότητας, και οι οποίες είναι ορισμένες σε ειδικώς
δομημένα μερικώς διατεταγμένα σύνολα, τα οποία ονομάζουμε δομές
λεξικογραφικού πλέγματος. Όταν το θεώρημα εφαρμόζεται σε μονοτονικές
συναρτήσεις, δίνει ως ειδική περίπτωση το κλασικό θεώρημα των Knaster-Tarski.
Η αρχική απόδειξη του θεωρήματος, όπως παρουσιάζεται στο LICS 2020, είναι
κατασκευαστική. Η προτεινόμενη απόδειξη είναι πιο απλή από την αρχική και δίνει
μια εναλλακτική διαίσθηση και περαιτέρω εμβάθυνση στο θεώρημα σταθερού σημείου.
Επιπροσθέτως, αποδεικνύουμε ότι τα σύνολα των προ-σταθερών, μετα-σταθερών, και
σταθερών σημείων των συναρτήσεων πάνω σε αυτές τις δομές, σχηματίζουν πλήρη
πλέγματα. Οι αποδείξεις μας έχουν επαληθευτεί μέσω του Coq. Τα αποτελέσματά μας
έχουν άμεσες εφαρμογές σε περιοχές της Πληροφορικής, όπου χρησιμοποιούνται
μη-μονοτονικοί φορμαλισμοί, όπως στην Τεχνητή Νοημοσύνη, στο Λογικό
Προγραμματισμό και στη Θεωρία Τυπικών Γλωσσών.
(EL)
In this thesis, we develop a novel, non-constructive proof of the fixed point
theorem proposed by A. Charalambidis, G. Chatziagapis and P. Rondogiannis
(LICS20). This theorem proves the existence of a least fixed point of
functions that possess a restricted form of monotonicity, and are defined
over some specially structured partially ordered sets, which we will call
lexicographic lattice structures. Our results give as a special case
the well-known Knaster-Tarski theorem when restricted to monotonic functions.
The initial proof of the theorem, as presented at LICS 2020, is constructive.
Our novel proof is simpler and it gives an alternative intuition and a deeper
understanding of the theorem. Furthermore, we prove that the sets of pre-fixed,
post-fixed and fixed points of function over those structures form a complete
lattice. Our proofs have been verified through the Coq proof assistant. Our
results have direct applications in fields of Computer Science where
non-monotonic formalisms are being used, such as Artificial Intelligence, Logic
Programming and Formal Language Theory.
(EN)
/aggregator-openarchives/portal/institutions/uoa
