Algebrai struktúrák és fixpont műveletek a számítástudományban
Title in English
Algebraic structures and fixed point operations in computer science
Keywords in Hungarian
iterációs félgyűrűk és félmodulusok, iterációs elméletek, fixpont műveletek, ekvacionális logika
Keywords in English
iteration semirings and semimodules, iteration theories, fixed point operations, equational logic
Discipline
Mathematics (Council of Physical Sciences)
100 %
Ortelius classification: Algebra
Panel
Mathematics and Computing Science
Department or equivalent
Institute of Informatics (University of Szeged)
Starting date
2014-07-01
Closing date
2016-06-30
Funding (in million HUF)
3.984
FTE (full time equivalent)
0.50
state
closed project
Summary in Hungarian
A kutatás összefoglalója, célkitűzései szakemberek számára Itt írja le a kutatás fő célkitűzéseit a témában jártas szakember számára. A számítástudományban a rekurzív definíciók és az iteráció szemantikáját általában függvények, funktorok vagy egyéb konstruktorok fixpontjaival írják le. Vizsgálni kívánjuk a fixpont műveletek azonosságait a félgyűrűkben és félmodulusokban, és általánosabban, a Lawvere elméletekben és a Descartes-féle kategóriákban.
Mi a kutatás alapkérdése? Ebben a részben írja le röviden, hogy mi a kutatás segítségével megválaszolni kívánt probléma, mi a kutatás kiinduló hipotézise, milyen kérdéseket válaszolnak meg a kísérletek. Korábbi vizsgálatok megmutatták, hogy lényegében minden a számítástudományban felhasznált Decartes-féle fixpont modell pontosan az iterációs elméletek azonosságait elégíti ki. Az egyik vizsgálandó kérdés az iterációs elméletek axiómáinak egyszerűsítését tűzi ki, esetleg további műveletek, pld. additív struktúra jelenlétében. Ebben az esetben a kérdés az iterációs félgyűrűkre és félmodulosokra vonatkozó kérdésnek felel meg. Egy másik kérdés az iterációs elméletek és iterációs félgyűrűk és félmodulusok felhasználása a szamítástudományban axiomatikus kérdések megoldására.
Mi a kutatás jelentősége? Röviden írja le, milyen új perspektívát nyitnak az alapkutatásban az elért eredmények, milyen társadalmi hasznosíthatóságnak teremtik meg a tudományos alapját. Mutassa be, hogy a megpályázott kutatási területen lévő hazai és a nemzetközi versenytársaihoz képest melyek az egyediségei és erősségei a pályázatának! Teljes (első-rendű) axiómarendszerek megalkotása a számítástudomány több területén alapvető kérdés. Rengeteg vizsgálat irányult az átmeneti rendszerek szekvenciális és konkurens viselkedésének vagy a folyamatábra programok axiomatizálására, a véges és végtelen szavakból vagy fákból álló reguláris nyelvek axiomatizálására, a dinamikus logika és az akció logikák axiomatikus tárgyalására, stb. Mivel ezek mindegyike tartalmazza a fixpont művelet valamely formáját, ezért azt várjuk, hogy a javasolt kutatás ezen elméletek egyszerűbb és jobb axiomatizálásához vezet.
A kutatás összefoglalója, célkitűzései laikusok számára Ebben a fejezetben írja le a kutatás fő célkitűzéseit alapműveltséggel rendelkező laikusok számára. Ez az összefoglaló a döntéshozók, a média, illetve az érdeklődők tájékoztatása szempontjából különösen fontos az NKFI Hivatal számára. A legtöbb számítógépes alkalmazásban megtalálhatók olyan specifikációk, amelyek rekurzív definíciót is felhasználnak. A számítástudomány nagy mértékben a specifikációk, és a specifikációk azonos vagy különböző absztrakciós szintek közti átalakításának művészete. A javasolt kutatás potenciálisan hozzájárulhat a specifikációk átalakítására általánosan és specifikusan is alkalmazható hatékony módszerek kifejlesztéséhez.
Summary
Summary of the research and its aims for experts Describe the major aims of the research for experts. The semantics of recursion and iteration in computer science is usually captured by fixed points of functions, functors, or other constructors. We propose to study the equational properties of fixed point operations in semirings, semimodules, and more generally, in Lawvere theories, or cartesian categories.
What is the major research question? Describe here briefly the problem to be solved by the research, the starting hypothesis, and the questions addressed by the experiments. It has been shown that all reasonable cartesian fixed point models used in computer science satisfy exactly the identities of iteration theories. One of the questions of the proposed study aims at the simplification of the axioms of iteration theories, possibly in the presence of other operations, such as an additive structure, when the problem can be reduced to corresponding questions regarding iteration semirings and iteration semiring-semimodule pairs in which linear equations have canonical solutions. A second question concerns the application of of iteration theories and iteration semirings and semiring-semimodule pairs to axiomatization problems in computer science.
What is the significance of the research? Describe the new perspectives opened by the results achieved, including the scientific basics of potential societal applications. Please describe the unique strengths of your proposal in comparison to your domestic and international competitors in the given field. Finding complete (first-order) axiomatizations has always been a major problem in many branches of theoretical computer science. There has been an enormous amount of effort devoted to finding appropriate axioms for the sequential and concurrent behavior of transition systems, flowchart behavior, finitary and infinitary regular languages, tree languages, dynamic logic, action logics, and other structures and theories. Since all of these structures and theories contain a fixed point operation, the proposed research would lead to simpler and better axioms for all of them.
Summary and aims of the research for the public Describe here the major aims of the research for an audience with average background information. This summary is especially important for NRDI Office in order to inform decision-makers, media, and others. Most computer applications involve some form of specifications which in turn often involves recursive definitions. Computer science is to a large extent the art of specification and transformation of specifications at the same or between different levels of abstraction. The proposed research has the potential of developing efficient methods for transforming specifications into simpler equivalent specifications both in general and concrete settings.
