Yes (75637)
No (328)
Used filters
(2)
Number of found documents:
75965
Published from
to
Combining effects with dependent types
Mückenschnabel, Maya; Petříček, Tomáš; Šefl, Vít
2024 - Czech
Dependent type systems provide a novel way of reasoning about program correctness, by embedding behavior of the program into the more expressive type system. Correctness is achieved by not allowing incorrect states to be representable. Languages like Idris show that dependent type systems are practically useful, not only for formal proofs, but also for creating fewer bugs in production. But the purity of computation poses a problem for composability of stateful computations and of side effects. Effect handlers provide one possible solution for this problem. In this thesis we propose an effect extension of depen- dent type systems. The resulting system not only makes it possible to provide guarantees about correctness of a program, but also make it easy to compose such guarantees using effects. We formalize the type system and present a prototype implementation.
Keywords:
dependent types|effect handlers|type systems; dependent types|effect handlers|type systems
Available in a digital repository NRGL
Combining effects with dependent types
Dependent type systems provide a novel way of reasoning about program correctness, by embedding behavior of the program into the more expressive type system. Correctness is achieved by not allowing ...
Experimentální analýza dotazovacích jazyků v moderních databázových systémech
Čorovčák, Martin; Koupil, Pavel; Holubová, Irena
2024 - English
The rise of Big Data has highlighted the limitations of relational databases while handling large datasets, leading to the growth of NoSQL databases. This has made DBMS benchmarking crucial for performance evaluation and decision-making. This thesis compares relational (MySQL, SQLite), graph (Neo4j, ArangoDB), docu- ment (MongoDB), and column-family (Cassandra) databases. We analyze the expressive power of their query languages and their runtime efficiency across varying data sizes. We conclude, that there's no "number one" solution for all use cases. The choice depends on factors like data volume, query complexity, and the need for joins. For complex queries and frequent joins, MySQL and SQLite are the most expressive but may struggle with very large datasets. Cassandra and MongoDB excel in perfor- mance and scalability but require efficient schema design and targeted data redundancy. ArangoDB presents a versatile option capable of handling multiple data models but might require further investigation into its performance compared to Neo4j. Príchod Vel'kých Dát poukázal na obmedzenia relačných databáz pri spracovanível'kých datasetov, čo viedlo k nárastu NoSQL databáz. Z tohto dôvodu sa DBMS benchmarking stal kl'účovým pre hodnotenie výkonnosti a celkový rozhodovací proces. Táto práca porovnáva relačné (MySQL, SQLite), grafové (Neo4j, ArangoDB), doku- mentové (MongoDB) a stĺpcovo-orientované (Cassandra) databázy. Analyzujeme vyja- drovaciu silu ich dopytovacích jazykov a efektivitu počas behu pri rôznych vel'kostiach dát. Dospeli sme k záveru, že neexistuje žiadne riešenie "číslo jeden" pre všetky prípady použitia. Výber závisíod faktorov, ako je objem dát, zložitost' dopytov a potreba spájania. V prípade zložitých dotazov a častého spájania majú MySQL a SQLite najv̈ačšiu vy- jadrovaciu silu, avšak môžu mat' problémy s vel'mi vel'kými datasetmi. Cassandra a Mon- goDB vynikajú výkonom a škálovatel'nost'ou, ale vyžadujú efektívny návrh schématu a cielenú redundanciu dát. ArangoDB predstavuje univerzálnu možnost', ktorá dokáže pra- covat' s viacerými dátovými modelmi, ale pre hlbšie porovnanie s Neo4j sa môže vyžadovat' d'alší výskum ich výkonu.
Keywords:
databázové systémy|výkon|benchmark|statická analýza|experimentální analýza; database management systems|performance|benchmark|static analysis|experimental analysis
Available in a digital repository NRGL
Experimentální analýza dotazovacích jazyků v moderních databázových systémech
The rise of Big Data has highlighted the limitations of relational databases while handling large datasets, leading to the growth of NoSQL databases. This has made DBMS benchmarking crucial for ...
Jak výkonnostní sport ovlivňuje stravování dětí a rozvoj poruch příjmu potravy
Černá, Renata; Floriánková, Marcela; Kosheleva, Svetlana
2024 - Czech
5 ABSTRACT The theoretical part of the bachelor's thesis addresses the issue of eating disorders with a focus on children and adolescents and it also explores the influence of sports, particularly at the high- performance level, on the nutritional needs of children and adolescents, as well as the risk of developing an eating disorder. The practical part compares selected parameters of children in the 4th year of elementary school (comparing sports and regular classes) and in the 6th year of elementary school (comparing sports and regular classes). It involves monitoring anthropometric data, the correlation between subjective perception of one's own weight and its objective assessment, food choices with regard to their effects on health, weight and performance, adherence to dietary measures, the presence of targeted weight loss in the last 6 months, the intensity of regular physical activity, and selected factors of the external environment that are considered risky in terms of the development of eating disorders. There was no statistically significant difference in the BMI of children from the sports class and the regular class in the first stage, but the BMI of children from the sports class was statistically significantly lower (p < 0.001) in the second grade. In other parameters, there was no significant... 4 ABSTRAKT Bakalářská práce ve své teoretické části pojednává o problematice poruch příjmu potravy (PPP) se zaměřením na děti a adolescenty a zároveň vlivu sportu, zejména provozovanému na výkonnostní úrovni, na nutriční potřeby dětí a dospívajících a na riziko rozvoje poruchy příjmu potravy. Praktická část je věnována srovnání vybraných parametrů u dětí ve 4. ročníku základní školy (porovnání sportovní a běžné třídy) a v 6. ročníku ZŠ (porovnání sportovní a běžné třídy). Sledovány byly antropometrické údaje, korelace mezi subjektivním vnímáním vlastní hmotnosti a jejím objektivním posouzením, výběr potravin s ohledem na jejich vliv na zdraví, hmotnost a výkon, dodržování dietních opatření, přítomnost cíleného hubnutí v posledních 6 měsících, intenzita pravidelné pohybové aktivity a vybrané faktory vlivu vnějšího prostředí, které jsou považovány za rizikové z hlediska rozvoje PPP. Ve sledovaném souboru nebyl zjištěn statisticky významný rozdíl v BMI dětí ze sportovní a běžné třídy na prvním stupni, na druhém stupni byl BMI dětí ze sportovní třídy statisticky významně nižší (p <0,001). V ostatních parametrech nebyl zjištěn významný rozdíl mezi dětmi ze sportovních a běžných tříd - nelišil se podíl dětí, které cíleně hubly, dodržovaly dietní opatření, nelišil se významně podíl dětí, které měly zkreslené...
Keywords:
poruchy příjmu potravy; výkonnostní sport; dětství; adolescence; mentální anorexie; mentální bulimie; eating disorder; high-performance sport; childhood; adolescence; anorexia nervosa; bulimia nervosa
Available in a digital repository NRGL
Jak výkonnostní sport ovlivňuje stravování dětí a rozvoj poruch příjmu potravy
5 ABSTRACT The theoretical part of the bachelor's thesis addresses the issue of eating disorders with a focus on children and adolescents and it also explores the influence of sports, particularly at ...
Procesy slabé saturace v multipartitních hypergrafech
Rajský, Adam; Tyomkyn, Mykhaylo; Tancer, Martin
2024 - Czech
Given hypergraphs H and P, wsat(H, P) denotes the smallest number of edges in a subgraph of H with the property that the missing edges can be sequentially added such that the addition of every edge creates a new copy of P. In 1985 Alon proved that wsat(Kn, P)/n tends to a finite limit for any graph P. A generalisation of this Theorem to r-uniform hypergraphs was conjectured by Tuza in 1992 and proved by Shapira and Tyomkyn in 2021. In this thesis, we use the methodology introduced by Shapira and Tyomkyn to prove a similar theorem when H is a complete r-partite r- uniform hypergraph. Dané hypergrafy H a P, wsat(H, P) označuje najmenší počet hrán v podgrafe H s vlastnosťou, že chýbajúce hrany možno postupne pridať tak, že pridanie každej hrany vytvorí novú kópiu P. V roku 1985 Alon dokázal, že wsat(Kn, P)/n konverguje k vlastnej limite pre akýkoľvek graf P. Tuza sa v roku 1992 domnieval, že platí zobecnenie tejto vety pre r-uniformné hypergrafy a dokázali ho Shapira a Tyomkyn v roku 2021. V tejto práci používame metodológiu, ktorú zaviedli Shapira a Tyomkyn, aby sme dokázali podobnuú vetu, v ktorej H je úplný r-partitný r-uniformný hypergraf.
Keywords:
wsat|slabá saturácia|hypergraf|extremálna kombinatorika; wsat|weak saturation|hypergraph|extremal combinatorics
Available in a digital repository NRGL
Procesy slabé saturace v multipartitních hypergrafech
Given hypergraphs H and P, wsat(H, P) denotes the smallest number of edges in a subgraph of H with the property that the missing edges can be sequentially added such that the addition of every edge ...
Framework pro interaktivní distribuovanou síť světelných zařízení
Kurek, Daniel; Obdržálek, David; Vodrážka, Jindřich
2024 - Czech
This work presents a framework for interactive appliaction on a distributed network of lighting devices based on Espressif ESP32-S3 modules. The framework locates devices by measuring their mutual distances. There are two types of devices, fixed stations and mobile devices, due to the intended use of the framework. The work also includes a helping application for a PC that visualizes the localization and allows direct control of devices. The framework uses Bluetooth mesh for communication and WiFi FTM (RTT) for distance measurement. To test the framework, physical devices were designed and fabricated. The framework and fabricated devices are demonstrated in a 'Find Your Color' game where the goal is to bring mobile device to a fixed station with the same color as the mobile device. Tato práce představuje framework pro práci s distribuovanou sítí světelných zaří- zení založených na modulech Espressif ESP32-S3. Framework lokalizuje zařízení na zá- kladě měření jejich vzájemných vzdáleností, přičemž vzhledem k plánovanému použití frameworku rozlišuje mezi pevně umístěnými stanicemi a mobilními zařízenimi. Součástí práce je i pomocná aplikace pro osobní počítač, která vizualizuje lokalizaci a umožňuje přímé ovládání (nastavení) zařízení. Pro komunikaci framework používá Bluetooth mesh a pro měření vzdáleností WiFi FTM (RTT). K otestování frameworku byla navržena a vyrobena fyzická zařízení. Framework a vyrobená zařízení jsou předvedeny na hře 'Najdi svoji barvu', kde je cílem dojít s mobilním zařízením k pevně umístěné stanici se stejnou barvou, jako má mobilní zařízení.
Keywords:
Bluetooth mesh|lokalizační systém|distribuovaná síť; Bluetooth Mesh|Localization System|Distributed Network
Available in a digital repository NRGL
Framework pro interaktivní distribuovanou síť světelných zařízení
This work presents a framework for interactive appliaction on a distributed network of lighting devices based on Espressif ESP32-S3 modules. The framework locates devices by measuring their mutual ...
Online hry na podporu výuky "nové" informatiky na druhém stupni základní školy
Bohatová, Zuzana; Pešková, Klára; Forstová, Lenka
2024 - Czech
The thesis describes the development of the web application Starting With Computer Science (Začínáme s informatikou) for teaching computer science at the lower secondary level (ISCED 2). The application contains five themes. Each topic is divided into an in- troductory theoretical section and an interactive part. For example, it includes activities such as matching pairs on the topic of data storage, assembling a computer mother- board, or finding a path in a graph. In the thesis, the newly updated Czech national computing curriculum for lower secondary education, known as New Informatics, is in- troduced, followed by an analysis of existing interactive educational websites.Then we present an analysis of our solution, the user and application development documentation. Finally, we review the progress and results from testing the application with third-year students at an eight-year gymnasium. Práce popisuje vývoj webové aplikace Začínáme s informatikou pro výuku informatiky na druhém stupni základní školy. Aplikace obsahuje pět témat. Každé téma je rozděleno na úvod do teorie a interaktivní část. Najdeme zde pexeso na téma ukládání dat, mož- nost poskládat základní desku počítače nebo najít cestu v grafu a další. V textu práce je nejprve představen revidovaný vzdělávací program pro základní vzdělávání v oblasti Informatika, tzv. nová informatika a jsou zanalyzovány již existující interaktivní výukové weby. Dále představíme analýzu našeho řešení, uživatelskou a vývojovou dokumentaci aplikace. Závěrem projdeme průběh a výsledky testování aplikace na nižším stupni osmi- letého gymnázia.
Keywords:
výuková hra|nové RVP ZV|druhý stupeň základní školy; educational game|new curriculum framework|ISCED 2
Available in a digital repository NRGL
Online hry na podporu výuky "nové" informatiky na druhém stupni základní školy
The thesis describes the development of the web application Starting With Computer Science (Začínáme s informatikou) for teaching computer science at the lower secondary level (ISCED 2). The ...
AgentLang - Programovací jazyk pre agentovo orientované modelovanie
Boďa, Tomáš; Petříček, Tomáš; Bednárek, David
2024 - English
With the increasing popularity of the agent-based simulation technique in various scientific fields, there is a demand for an all-in-one framework for modeling agent-based simulations. Although there are numerous agent-based tools available, these in most cases feature complex syntax and language structures or are aimed to be used in specific domains only. In response this thesis presents a new approach to modeling agent-based simulations by developing a brand new agent-based framework - AgentLang. The frame- work features a programming language with a unified and simple syntax for defining agents and their properties. Moreover, it provides a web-based interface with a spread- sheet module for manipulating agents and their values using the familiar spreadsheet format as well as a visualisation module for rendering the simulation in real-time. These three features of the AgentLang framework aim to introduce a new way to modeling agent-based simulations and attempt to make agent-based modeling more accessible to people of all scientific fields. S rastúcou popularitou techniky agentovo orientovaného modelovania v rôznych ve- deckých oblastiach vzniká dopyt po jednotnom nástroji na modelovanie simulácií. Aj keď je na trhu dostupné množstvo nástrojov na agentovo orientované modelovanie, vo vač- šine prípadov sa vyznačujú zložitou jayzkovou syntaxou a štruktúrou alebo sú určené na použitie iba v špecifických oblastiach. Vzhľadom na tieto nevýhody táto práca poskytuje nový pohľad na agentovo orientované modelovanie tým, že vyvíja nový nástroj na mo- delovanie agentovo orientovaných simulácií - AgentLang. Tento nástroj poskytuje nový programovací jazyk s jednotnou, ucelenou a jednoduchou syntaxou na definovanie agen- tov a ich vlastností. Okrem toho poskytuje webovú aplikáciu s tabulkovým rozhraním na manipuláciu agentov a ich hodnôt. V neposlednom rade obsahuje vizualizačný modul na zobrazovanie simulácií v reálnom čase. Tieto tri vlastnosti nástroja AgentLang majú za cieľ poskytnúť nový spôsob modelovania agentovo orientovaných simulácií a sprístupniť agentovo orientované modelovanie používateľom zo všetkých vedeckých odvetví.
Keywords:
agentovo orientované modelovanie|simulácie|programovací jayzk|interpreter; agent-based modeling|simulation|programming language|interpreter
Available in a digital repository NRGL
AgentLang - Programovací jazyk pre agentovo orientované modelovanie
With the increasing popularity of the agent-based simulation technique in various scientific fields, there is a demand for an all-in-one framework for modeling agent-based simulations. Although there ...
Průhlednost nezávislá na pořadí
Rožek, Matúš; Kahoun, Martin; Iser, Tomáš
2024 - English
Rendering transparent geometry in realtime brings a set of problems as the transpar- ent objects need to be sorted first and rendered in order from back to front for their correct overlaying. A set of rendering algorithms called Order Independent Transparency (OIT) tries to accomplish this without sorting the geometry in advance. We create a program implementing five algorithms and compare their weaknesses, strengths, and properties. Some algorithms might excel in certain conditions and produce great results, yet fall short in slightly different environments. We aim to answer the question of which OIT algorithm is best suited for which scenarios. Vykresľovanie priehľadnej geometrie v reálnom čase spôsobuje sadu problémov, pre- tože jednotlivé objekty potrebujú byť zoradené a vykreslené v poradí odzadu dopredu pre korektný výsledok. Existuje avšak trieda algoritmov, ktorá sa snaží o vykreslenie obrazu aj bez potreby priehľadné objekty najprv zoradiť. Tieto algoritmy sa nazývajú "priehľadnosť nezávislá na poradí" (anglicky Order Independent Transparency, skratka OIT). Vytvorili sme program, ktorý obsahuje 5 rôznych OIT algoritmov. Poukazujeme na silné a slabé stránky jednotlivých prístupov - niektoré môžu excelovať v určitých pod- mienkach, ale zato podávať výrazne slabšie výsledky v odlišnom prostredí. Snažíme sa odpovedať na otázku, ktorý OIT algoritmus je najlepšie využiť v akej situácii.
Keywords:
priehľadnosť nezávislá na poradí|vykresľovanie priehľadnosti|alfa kompozícia|realtime rendering; order independent transparency|transparency rendering|alpha compositing|realtime rendering
Available in a digital repository NRGL
Průhlednost nezávislá na pořadí
Rendering transparent geometry in realtime brings a set of problems as the transpar- ent objects need to be sorted first and rendered in order from back to front for their correct overlaying. A set of ...
Klasifikace autorství textu s neznámým autorem
Dolník, Karel; Hajič, Jan; Mírovský, Jiří
2024 - Czech
Statistical and computational authorship attribution is a widely researched topic in literary science, but few works deal with solving the problem when the classified text does not belong to any of the authors the model saw during training. This work seeks a way to detect such an unknown author using machine learning methods commonly used for authorship attribution, especially the SVM classifier. He we introduce a modified One-versus-Rest-and-None classification scheme, which extends the One-versus-Rest scheme by training with data that does not belong to any classified author. This can be done using synthetically produced data or data from authors who are certain to have no connection to the classified texts. It turned out that the smallest decrease in accuracy occurred when synthetic data is used, compared to the classification without detection of an unknown author. Přiřazení autorství pomocí statistických a výpočetních metod je hojně zkoumaným tématem literární vědy, ovšem jen málo prací se zabývá řešením problému, kdy klasifikovaný text nenapsal nikdo z autorů, které model viděl při trénování. Tato práce hledá způsob, jak takového neznámého autora detekovat v rámci stejných metod strojového učení, které se pro přiřazení autorství běžně používají, zejména klasifikátoru SVM. Zavádíme zde upravené klasifikační schéma One-versus-Rest-and-None které rozšiřuje schéma One-versus-Rest o trénování pomocí dat, která nepatří žádnému klasifikovanému autorovi. K tomu lze využít synteticky vytvořená data, nebo data od autorů, u kterých je jisté, že s klasifikovanými texty nejsou nijak spojeni. Ukázalo se, že právě při použití syntetických dat dojde k nejmenšímu snížení přesnosti oproti klasifikaci bez detekce neznámého autora.
Keywords:
klasifikace autorství|strojové učení|výpočetní literární věda|stylometrie; authorship classification|machine learning|computational literary science|stylometry
Available in a digital repository NRGL
Klasifikace autorství textu s neznámým autorem
Statistical and computational authorship attribution is a widely researched topic in literary science, but few works deal with solving the problem when the classified text does not belong to any of ...
Zjednodušení použitelnosti nástrojů pro správu kvality dat pro datové inženýry
Tomis, Zdeněk; Bulej, Lubomír; Škoda, Petr
2024 - English
In the realm of data quality management, integrating robust data quality rules into automated workflows and data pipelines is essential for maintaining data integrity. This thesis addresses the gap in programmatic accessibility of Ataccama ONE's data qual- ity tools, which primarily leverage the proprietary Ataccama Expression Language. By reimplementing this language in Python, the project enhances its usability for data en- gineers who seek to consume these tools programmatically. The focus is on enabling data engineers to execute Ataccama's rules directly within Python. The viability of this implementation is tested through performance comparisons with similar solutions. V oblasti data quality managementu je pro zachování integrity dat zásadní integrovat pravidla kvality dat do automatizovaných workflows a datových pipelines. Tato práce se zabývá mezerou v programové dostupnosti nástrojů pro kvalitu dat společnosti Ataccama ONE, které využívají především proprietární jazyk Ataccama Expression Language. Re- implementací tohoto jazyka v jazyce Python projekt zvyšuje jeho použitelnost pro datové inženýry, kteří potřebují tyto nástroje využít programmaticky v různým prostředích. Dů- raz je kladen na to, aby datoví inženýři mohli provádět a spravovat pravidla Ataccama přímo v jazyce Python s ohledem na jednoduchost užití a minimální nároky. Užitelnost této implementace je otestována prostřednictvím porovnání výkonu s podobnými řeše- ními.
Keywords:
data quality management|data engineering|performance evaluation; data quality management|data engineering|performance evaluation
Available in a digital repository NRGL
Zjednodušení použitelnosti nástrojů pro správu kvality dat pro datové inženýry
In the realm of data quality management, integrating robust data quality rules into automated workflows and data pipelines is essential for maintaining data integrity. This thesis addresses the gap in ...
NRGL provides central access to information on grey literature produced in the Czech Republic in the fields of science, research and education. You can find more information about grey literature and NRGL at service web
Send your suggestions and comments to nusl@techlib.cz
Provider
Other bases