Algebrai struktúrák és fixpont műveletek a számítástudományban  részletek

súgó  nyomtatás 
vissza »

 

Projekt adatai

 
azonosító
110883
típus ANN
Vezető kutató Ésik Zoltán
magyar cím Algebrai struktúrák és fixpont műveletek a számítástudományban
Angol cím Algebraic structures and fixed point operations in computer science
magyar kulcsszavak iterációs félgyűrűk és félmodulusok, iterációs elméletek, fixpont műveletek, ekvacionális logika
angol kulcsszavak iteration semirings and semimodules, iteration theories, fixed point operations, equational logic
megadott besorolás
Matematika (Műszaki és Természettudományok Kollégiuma)100 %
Ortelius tudományág: Algebra
zsűri Matematika–Számítástudomány
Kutatóhely Informatikai Intézet (Szegedi Tudományegyetem)
projekt kezdete 2014-07-01
projekt vége 2016-06-30
aktuális összeg (MFt) 3.984
FTE (kutatóév egyenérték) 0.50
állapot lezárult projekt
magyar összefoglaló
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.
angol összefoglaló
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.




vissza »