• Definujte mieru aktuálnosti riešeného problému v danej oblasti vedy a techniky, z celosvetového pohľadu vrátane relevantných odkazov na odbornú literatúru
• Definujte vedeckú úroveň projektu a vedeckosť metód využívaných v riešení projektu
• Definujte ciele projektu a reálnosť ich dosiahnutia
• Opíšte navrhovanú metodiku riešenia projektu, opodstatnenosť jej výberu a efektívnosť jej pouţitia z hľadiska splnenia deklarovaných cieľov

Jeden z najväčších objavov minulého storočia v oblasti informatiky a logiky bolo formulovanie Curry-Howardovho izomorfizmu [1]. Tento izomorfizmus opisuje korešpondenciu medzi formulami a typmi, programami a dôkazmi. Táto korešpondencia odhalila, že dôkazy intuicionistickej logiky môžu byť preložené do λ-termov a vice versa [2]. Túto teóriu neskôr rozšíril Joachim Lambek o korešpondenciu s teóriou kategórií, ktorá je dnes známa pod názvom Curry-Howard-Lambekov izomorfizmus (CHL).

Curry-Howard-Lambekov izomorfizmus je aktuálnou témou skúmania mnohých výskumníkov [4]. Aplikácia výsledkov tohto výskumu sa využíva v rôznych oblastiach informatiky a matematiky, medzi ktoré patria automatické dokazovacie systémy [5-6], interaktívne dokazovacie systémy [7-9], tvorí taktiež základ automatickej typovej kontroly, resp. automatického odvodenia typov v mnohých programovacích jazykov [10-11]. Prostredníctvom intuicionistickej logiky a CHL je možné generovanie korektných programov z dôkazov ich špecifikácií [12].

V našom prístupe sa budeme venovať korešpondencii medzi jednoducho typovaným λ-kalkulom, Brouwer-Heyting-Kolmogorovou interpretáciou intuicionistickej logiky a teóriou kategórií. Vyhodnotenie termov λ-kalkulu korešponduje s metódou zjednodušovania dôkazov formúl intuicionistickej logiky v Gentzenovej prirodzenej dedukcii. V tomto projekte sa zameriame na túto časť CHL. Formulujeme nový spôsob vyhodnotenia λ-termov v pojmoch teórie kategórií prostredníctvom koalgebry polynomiálneho endofunktora vzhľadom na CHL, navyše konkrétna špecifikácia a definícia polynomiálneho endofunktora nám umožní modelovať správanie sa rožných redukčných stratégií v danej koalgebre.

Zdroje:

[1] Howard, W. A. (1980). The formulae-as-types notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 44, 479-490.

[2] Lecomte, A. (2011). Meaning, logic and ludics. World Scientific.

[3] Poernomo, I., Crossley, J. N., & Wirsing, M. (2005). Adapting Proofs-as-Programs: The Curry--Howard Protocol. Springer Science & Business Media.

[4] Zach, R. (2019, November). The Significance of Curry-Howard Isomorphism. In Philosophy of Logic and Mathematics. Proc. of the 41st International Ludwig Wittgenstein Symposium/Eds.: GM Mras, P. Weingartner, B. Ritter. Berlin: DeGruyter (pp. 313-326).

[5] Loveland, Donald W. Automated theorem proving: A logical basis. Elsevier, 2016.

[6] Bibel, Wolfgang. Automated theorem proving. Springer Science & Business Media, 2013.

[7] Nipkow, T., Wenzel, M., & Paulson, L. C. (Eds.). (2002). Isabelle/HOL: a proof assistant for higher-order logic. Berlin, Heidelberg: Springer Berlin Heidelberg.

[8] Geuvers, H. (2009). Proof assistants: History, ideas and future. Sadhana, 34(1), 3-25.

[9] Huet, G., Kahn, G., & Paulin-Mohring, C. (1997). The coq proof assistant a tutorial. Rapport Technique, 178.

[10] Gundry, A. M. (2013). Type inference, Haskell and dependent types.

[11] Damas, L., & Milner, R. (1982, January). Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 207-212).

[12] Bates, J. L., & Constable, R. L. (1985). Proofs as programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 7(1), 113-136.


Definujte vedeckú úroveň projektu a vedeckosť metód využívaných v riešení projektu. Definujte ciele projektu a reálnosť ich dosiahnutia

Ciele projektu spĺňajú požiadavku na vedeckosť. Cieľom projektu je formulácia sémantiky jednoducho typovaného λ-kalkulu prostredníctvom koalgebry polynomiálneho endofunktora v pojmoch teórie kategórií na základe Curry-Howard-Lambekovho izomorfizmu.

Použité metódy sú prísne exaktné a všetky prostriedky formálneho návrhu, ktoré budeme používať, sú matematicky dokázané. Skúsenosti a dosiahnuté výsledky nám dovoľujú považovať stanovené ciele za reálne a dosiahnuteľné v rámci doby riešenia projektu.

Opíšte navrhovanú metodiku riešenia projektu, opodstatnenosť jej výberu a efektívnosť jej použitia z hľadiska splnenia deklarovaných cieľov:

Semináre, pravidelné stretnutia riešiteľov, stanovenie čiastkových cieľov, publikovanie čiastkových výsledkov, kooperácia, výmena vedomostí, atď.

Odôvodnenie finančných nárokov

V rámci dosahovania stanovených cieľov je dôležité vedecké výsledky prezentovať na medzinárodných konferenciách a publikovať ich vo významných vedeckých časopisoch. Rovnako je dôležité získavať pravidelne nové informácie z danej oblasti. Z uvedeného dôvodu chceme získané prostriedky použiť nasledovne:

1. na úhradu konferenčných poplatkov (vložného) a cestovných nákladov na významné medzinárodné vedecké konferencie,
2. na pokrytie nákladov na nákup potrebnej odbornej literatúry,
3. na pokrytie nákladov na nákup spotrebného materiálu.

• Definujte mieru originálnosti projektu
• Opíšte navrhovaný koncept riešenia a formulujte vedeckú hypotézu
• Definujte význam predbežných výsledkov, nadväznosť navrhovaného riešenia na vlastné publikované výsledky

Vo všeobecnosti Curry-Howard-Lambekov izomorfizmus je funktor z kategórie λ-kalkulu do kategórie dôkazov, prostredníctvom ktorého je definovaná kategorická sémantika. V našom prístupe sa zameriame na novú metódu definície sémantiky λ-termov s dôrazom na ich postupné vyhodnocovanie, a to využitím koalgebry polynomiálneho endofunktora v pojmoch teórie kategórií. Relácia vyhodnotenia λ-termov v štrukturálnej operačnej sémantike je reflexívna a tranzitívne uzavretá, pričom tieto vlastností je možné exaktne modelovať koalgebrou polynomiálneho endofunktora a zároveň pri špecifikácii a definícii polynomiálneho endofunktora je možné sa zamerať na rôzne stratégie vyhodnocovania λ-termov.

Východisková hypotéza projektu je nasledovná:
„Výroky, dôkazy, a zjednodušenie dôkazov intuicionistickej logiky korešpondujú s typmi, programami, a vyhodnotením programov typovaného λ-kalkulu, tie korešpondujú s objektami, morfizmami kategórie typovaného λ-kalkulu, a koalgebrou polynomiálneho endofunktora nad kategóriou jednoducho-typovaného λ-kalkulu.“
Overenie našej hypotézy budeme realizovať napĺňaním vedeckých cieľov formulovaných vyššie.

Použité metódy, ako je jednoducho-typovaný λ-kalkul, intuicionistická logika a teória kategórií, sú prísne exaktné a všetky prostriedky formálneho návrhu, ktoré budeme používať, sú matematicky dokázané. Intuicionistická logika a jej dedukčný (dokazovací) systém umožnia logický dôkaz všetkých formulovaných vlastností modelu, čo bude zaručovať jeho korektnosť a spoľahlivosť. Definícia nášho modelu rozšíri spôsob pochopenia a možnosti definície nových programovacích jazykov, resp. pomôže pri formulovaní štruktúr programovacích jazykov.


Nadväznosť navrhovaného riešenia na vlastné publikované výsledky:

Ciele projektu nadväzujú na doterajší výskum v oblasti vývoja korektného softvéru využitím formálnych metód, výpočtových kalkulov, logických systémov a konštruovaniu behaviorálnych modelov netriviálnych systémov. Skúsenosti a dosiahnuté výsledky nám dovoľujú považovať stanovené ciele za reálne a dosiahnuteľné v rámci doby riešenia projektu.

Tento projekt nadväzuje na už realizované výsledky výskumu venovaného modelovaniu komplexných systémov ako sú systémy detekcie prienikov [1], prostredníctvom teórie kategórií [2], v pojmoch koalgebry polynomiálneho endofunktora [3], kategorickému modelovaniu typovaného λ-kalkulu s referenčnými typmi [4], jednoduchého funkcionálneho jazyka prirodzených čísel a pravdivostných hodnôt [5], [6], logickej analýze spracovania prirodzeného jazyka [7-10].


Literatúra:

[1] Perháč, J., Novitzká, V., Steingartner, W., & Bilanová, Z. (2021). Formal model of IDS based on BDI logic. Mathematics, 9(18), 2290.

[2] Perháč, J., & Mihályi, D. A. N. I. E. L. (2016). Coalgebraic specification of network intrusion signatures. Studia Universitatis Babes-Bolyai, Informatica, 61(2), 83-94.

[3] Perháč, J., & Mihályi, D. (2015, November). Coalgebraic modeling of IDS behavior. In 2015 IEEE 13th International Scientific Conference on Informatics (pp. 201-205). IEEE.

[4] Novitzká, V., Steingartner, W., & Perháč, J. A Simple Categorical Model of Reference Type. IPSI Transactions on Internet Research. - Belehrad (Srbsko) : IPSI Roč. 17, č. 2 (2021), s. 3-7 . - ISSN 1820-4503

[5] Perháč, J., & Bilanová, Z. (2020, September). Categorical Model of Functional Language with Natural Numbers and Boolean Values. In 2020 IEEE 15th International Conference on Computer Sciences and Information Technologies (CSIT) (Vol. 2, pp. 99-102). IEEE.

[6] Perháč, J., Bilanová, Z., & Havrilčáková, G. (2019). Simple-typed functional language modeled by category theory In: ICT in Education, Research, and Industrial Application : proceedings of the 15th international conference volume 3. - Aachen (Nemecko) : CEUR-WS s. 34-43 [online]. - ISSN 1613-007

[7] Novotný, S., Michalko, M., Perháč, J., Novitzká, V., & Jakab, F. (2022). Formalization and Modeling of Communication within Multi-Agent Systems Based on Transparent Intensional Logic. Symmetry, 14(3), 588.

[8] Bilanová, Z., & Perháč, J. (2019, May). About possibilities of applying logical analysis of natural language in computer science. In 2019 IEEE 13th International Symposium on Applied Computational Intelligence and Informatics (SACI) (pp. 251-256). IEEE.

[9] Bilanová, Z., Perháč, J., Chovancová, E., & Chovanec, M. (2020). Logic analysis of natural language based on predicate linear logic. Acta Polytechnica Hungarica, 17(6), 239-252.

[10] Bilanová, Z., & Perháč, J., (2019). Natural Language Dialogue Formalization: From Hyperintensional Logic to Linear Logic. In ICTERI PhD Symposium (pp. 44-52).

• Definujte harmonogram riešenia projektu s ohľadom na logickú nadväznosť postupov a na napĺňanie deklarovaných cieľov
• Vysvetlite adekvátnosť použitej metodiky
• Vysvetlite adekvátnosť navrhnutého rozpočtu projektu v kontexte finančnej náročnosti dosiahnutia cieľov
• Stanovte časový plán realizácie a naplnenia stanovených vedeckých cieľov

- Obdobie: 1.1.2023 – 28.2.2023:
Analýza potrebných formálnych aparátov:
- Teória kategórií.
- Brouwerova–Heytingova–Kolmogorovova interpretacia intuicionistickej logiky.
- Jednoducho typovaný λ-kalkul.
Dôraz bude kladený na korešpondenciu medzi vyhodnotením termov λ-kalkulu a metódou zjednodušovania dôkazov formúl intucionistickej logiky v gentzenovom dokazovaciom systéme - prirodzenej dedukcii.

- Obdobie: 1.3.2023 – 31.8.2023
Syntéza získaných poznatkov. Explicitná formulácia kategórie typovaného λ-kalkulu, špecifikácia a definícia polynomiálneho endofunktora nad konštruovanou kategóriou.
Sformulujeme kategóriu jednoducho typovaný λ-kalkulu ako karteziánsky uzavretú kategóriu. Objekty tejto kategórie budú reprezentovať typy a morfizmy budú reprezentovať termy jednoducho typovaného λ-kalkulu. Následne prejdeme k špecifikácii polynomiálneho endofunktora nad danou kategóriu so zameraním na rôzne redukčné stratégie.

- Obdobie: 1.9.2023 – 30.11.2023
Implementácia získaných poznatkov. Modelovanie vyhodnotenia termov λ-kalkulu prostredníctvom kolagebry polynomiálneho endofunktora nad konštruovanou kategóriou. Overenie konštruovaného modelu.
Skonštruujeme model sémantiky jednoducho typovaného λ-kalkulu ako koalgebru polynomiálneho endofunktora. Použitá špecifikácia a definícia polynomiálneho endofunktora bude reprezentovať konkrétny model pre určenú redukčnú stratégiu.

- Obdobie: 1.12.2023 – 31.12.2023
Príprava finálnej publikácie celkových dosiahnutých výsledkov riešenia projektu.


Adekvátnosť návrhu rozpočtu projektu:

Pre publikovanie čiastkových a celkových výsledkov a nadviazanie potenciálnej medzinárodnej spolupráce bude potrebná účasť na medzinárodných konferenciách.

• Odôvodnite kompetentnosť zúčastnených riešiteľských organizácií na riešenie predkladaného projektu v kontexte hlavných úloh, ktoré budú jednotlivé organizácie v projekte zabezpečovať
• Opíšte kompetentnosť jednotlivých riešiteľov na riešenie predkladaného projektu a základné úlohy, ktoré budú v rámci implementácie projektu realizovať (netýka sa zodpovedného riešiteľa)
• Opíšte spôsob kooperácie riešiteľov, ich vzájomnú komplementaritu a zastupiteľnosť pri riešení projektu
• Opíšte existujúcu prístrojovú a personálnu infraštruktúru pracovísk podieľajúcich sa na implementácii projektu
• Opíšte mieru zapojenia mladých pracovníkov výskumu a vývoja do 35 rokov vrátane študentov doktorandského štúdia do riešenia projektu

Ing. Ján Perháč, PhD. – vedúci projektu
Odborný asistent Katedry počítačov a informatiky.
Jeho hlavná vedecká orientácia sa zameriava na teóriu typov, neklasické logické systémy v informatike a konštruovanie formálnych modelov s využitím teórie kategórií. Jeho vedľajšia výskumná činnosť je orientovaná na sieťovú bezpečnosť, systémy na detekciu prienikov, komponentovo orientované programovanie.

Ing. Daniel Gecášek, PhD. – zástupca vedúceho projektu
Vedecko-výskumný pracovník UVP TECHNICOM. Jeho vedecká orientácia sa zameriava na automatizáciu fyzikálnych modelov v prostredí HPC a následné spracovanie vyprodukovaných dát.

Ing. Michal Solanik – riešiteľ
Interný doktorand Katedry počítačov a informatiky.
Jeho hlavná vedecká orientácia sa zameriava na akceleráciu fyzikálnych modelov v paralelnom a distribuovanom prostredí.

Bc. Samuel Novotný – riešiteľ
Študent katedry počítačov a informatiky v odbore Informatika s ašpiráciou na absolvovanie doktorandského štúdia. Jeho výskum je zameraný na formalizáciu rečových aktov v multiagentových systémoch prostredníctvom intenzionálnych logických systémov. V spoluautorstve s vedúcim projektu publikoval karentovaný článok v impaktovanom časopise (Q2).

Bc. Vitalii Tsimbolynets – riešiteľ
Študent katedry počítačov a informatiky v odbore Informatika. Jeho výskum je zameraný na vizualizáciu formálnych metód z oblasti teoretickej informatiky. Vedúci projektu je jeho budúcim školiteľom diplomovej práce, v minulosti aj bakalárskej práce.

Vo výskumnom tíme prezentovaného projektu sa nachádza jeden študent doktorandského štúdia, jeden odborný asistent Katedry počítačov a informatiky, dvaja študenti denného štúdia odboru Informatika v inžinierskom stupni a vedecko-výskumný pracovník UVP TECHNICOM. Výskumný tím je vytvorený tak, aby skúsenosti jeho členov adekvátne pokryli všetky skúmané oblasti. Hlavnými riešiteľmi projektu sú Ján Perháč, Vitalii Tsimbolynets, Samuel Novotný, ktorí budú skúmať spôsoby kategorického modelovania výpočtových systémov, CHL izomorfizmus, na základe čoho budú formulovať nový model sémantiky termov jednoducho typovaného λ-kalkulu. Ich úlohou je okrem iného zabezpečiť plynulý priebeh výskumných prác na projekte a odbornú konzultáciu pri praktickej aplikácii vytvoreného prístupu ďalším dvom spoluriešiteľom (Michal Solanik, Daniel Gecášek), ktorých úlohou bude zabezpečiť realizáciu vytvoreného riešenia spolu so sprístupnením modelu do vyučovacieho procesu predmetov Logika pre informatikov a Teória typov.

Opíšte spôsob kooperácie riešiteľov a ich vzájomnú komplementaritu:
Semináre, pravidelné stretnutia riešiteľov, stanovenie čiastkových cieľov, publikovanie čiastkových výsledkov, kooperácia, výmena vedomostí.

Opíšte existujúcu prístrojovú infraštruktúru na implementácii projektu:
Riešiteľský kolektív tvoria riešitelia z nasledujúcich pracovísk:
- Laboratórium informatiky a počítačových jazykov (Perháč).
- Laboratórium počítačových sietí (Gecašek)
- Laboratórium informačných systémov (Solanik, Gecáček).
- Študenti KPI (Novotný, Tsimbolynets)

Spomenuté laboratória sú adekvátne vybavené pre úspešnú realizáciu cieľov projektu. Disponujú modernými technológiami a všetkou potrebnou infraštruktúrou.