Search

In typed functional programming there is often the need for combining pure and monadic (or other effectful) computations, but the required lifting must be done manually by the programmer and may result in cluttered code. This thesis explores ways to allow the compiler to perform this task automat- ically. Several possible approaches are described, where the final one reduces the task to solving a system of linear diophantine equations. Apart from monads, the described method is also considered for the case of applicative functors as another abstraction to represent effectful operations. 1

In this thesis we address a long-term maintainability problem in Haskell type class system. In particular we study a possibility of backward-compatible changes in existing class hierarchies. In the first part of the thesis we give a brief overview of the language. The following part summarizes current proposed solutions to the problem and analyzes their properties. Based on this analysis we derive our own language extension proposal. In the penultimate chapter we present several possible applications of the language extension and compare the extension to other solutions. As a part of the thesis we also give a proof-of-concept implementation of the extension for the GHC compiler, which is briefly described in the last part of this thesis. Powered by TCPDF (www.tcpdf.org)

In this thesis is presented design and implementation of a system performing genetic programming in simply typed lambda calculus. Population initialization method based on term generating technique producing typed lambda terms in long normal form is introduced. This method is parameterized by simple search strategy. Several search strategies are presented, such as strategy for systematic generation or strategy corresponding to standard ramped half-and-half method. Another such a strategies called \textit{geometric} strategy is further examined in experiments and shown to have various desirable effects such as improved success rate, lesser time consumption and smaller average term size in comparison with standard ramped half-and-half generating method. Other performance enhancements are proposed and supported by experiments such as eta-normalization of generated individuals and @-tree representation of individuals. Abstraction elimination is utilized to enable use of simple tree- swapping crossover. Powered by TCPDF (www.tcpdf.org)

Automated theorem provers can be modified in order to use external sources of axioms. This was recently searched in combination with saturation based theorem prover SPASS-XDB. It sends queries to external sources and receives answers during its saturation loop. Lean theorem provers are based on semantic tableau calculus. That's why they need to use different approach. An idea that proving is separated from communication is beeing introduced by this work. Prover generetes so called schematic proof which is later checked if it can be filled with external data so the proof can be completed. This work demonstates this idea on modified version of LeanCoP.

Functional reactive programming provides mechanisms of describing dynamic systems in a declarative and type-safe manner, which is traditional domain of functional languages in general and Haskell, which we use here, in particular. We explore ways, in which it may be applied to programming web applications, specifically, we design a domain specific language intended for writing web pages as a part of a Haskell program, which would generate the actual code served to the client, and enriching them with dynamic content; and also find out to what extent we may broaden the expressive power of such library given certain inherent constraints of the chosen method. In doing so, we utilize the tree-like structure of the HTML page, which is quite suitable to be written as a source code in a programming language and to which we embed additional entities providing the dynamics and interactivity.

In the present thesis we deal with designing a program to play training games of mariáš (traditional czech card game) against computer. Two three-player versions of this game are considered - volený mariáš and licitovaný mariáš. The program enables to play games in tournament mode simulating the real game as well as in training mode where player can look into opponent's hand, undo moves, replay different variations, get advice from computer and so analyse the game situation. It is possible to extend the program by artificial players and to set up tournament between them. The thesis introduces several implementations of artificial player based on enchanced alfa-beta prunning.

This bachelor's thesis describes the main components of the program that simulates the car traffic. It describes the representation of road system, agents, simulation in progress and its output. It also describes several results reached during the simulation of concrete traffic situations. Moreover, the comparison between this program and multiagent systems is included in the end of this thesis. The road system consists of roads and crossroads which are controlled by traffic lights. The user of this program can observe different agent's behaviour. The only condition is that the class that represents an agent implements a uniform interface. The term agent means the car and its driver together. It is autonomous object that moves inside the road system respecting given limits of the simulation. Consequently, behaviour of agents is limited by the simulation rules. Agents are possibly controlled by simulation in order to avoid collisions and not to break traffic rules. The output of the simulation is used to compare the successfulness of individual strategies of agents in terms of length of the drive or fuel usage.