Paradygmaty Języków Programowania

dr Grzegorz Herman

środa 14:15-16:00, sala 0174

Poprzednie referaty

17.11.2021 12:15
Łukasz Selwa
 An Inverse of the Evaluation Functional for Typed λ-calculus by U. Berger and Η. Schwichtenberg
In any model of typed lambda-calculus containing some basic arithmetic, a functional p ->e (procedure —> expression) will be defined which inverts the evaluation functional for typed lambda-terms. Combined with the evaluation functional, p->e yields an efficient normalization algorithm. The method is extended to lambda-calculi with constants and is used to normalize (the lambda-representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for \beta \eta-reduction, generalizing results of Friedman and Statman. If two lambda-terms have the same value in some model containing
representations of the primitive recursive functions (of level 1) then they are provably equal in the \beta \eta-calculus.
10.06.2020 12:15
Wojciech Grabis
 Decidability of regular language genus computation by Guillaume Bonfante and Florian L. Deloup
This article continues the study of the genus of regular languages that the authors introduced in a 2013 paper (published in 2018). In order to understand further the genus g(L) of a regular language L, we introduce the genus size of |L|_gen to be the minimal size of all finite deterministic automata of genus g(L) computing L. We show that the minimal finite deterministic automaton of a regular language can be arbitrarily far away from a finite deterministic automaton realizing the minimal genus and computing the same language, in terms of both the difference of genera and the difference in size. In particular, we show that the genus size |L|_gen can grow at least exponentially in size |L|. We conjecture, however, the genus of every regular language to be computable. This conjecture implies in particular that the planarity of a regular language is decidable, a question asked in 1976 by R. V. Book and A. K. Chandra. We prove here the conjecture for a fairly generic class of regular languages having no short cycles. The methods developed for the proof are used to produce new genus-based hierarchies of regular languages and in particular, we show a new family of regular languages on a two-letter alphabet having arbitrary high genus.
10.06.2020 12:15
Wojciech Grabis
 Decidability of regular language genus computation by Guillaume Bonfante and Florian L. Deloup
This article continues the study of the genus of regular languages that the authors introduced in a 2013
paper (published in 2018). In order to understand further the genus g(L) of a regular language L, we
introduce the genus size of |L|gen to be the minimal size of all finite deterministic automata of genus g(L)
computing L.We show that the minimal finite deterministic automaton of a regular language can be arbitrarily
far away from a finite deterministic automaton realizing the minimal genus and computing the
same language, in terms of both the difference of genera and the difference in size. In particular, we show
that the genus size |L|gen can grow at least exponentially in size |L|. We conjecture, however, the genus of
every regular language to be computable. This conjecture implies in particular that the planarity of a regular
language is decidable, a question asked in 1976 by R. V. Book and A. K. Chandra. We prove here the
conjecture for a fairly generic class of regular languages having no short cycles. The methods developed
for the proof are used to produce new genus-based hierarchies of regular languages and in particular, we
show a new family of regular languages on a two-letter alphabet having arbitrary high genus.
10.06.2020 12:15
Wojciech Grabis
 Decidability of regular language genus computation by Guillaume Bonfante and Florian L. Deloup
This article continues the study of the genus of regular languages that the authors introduced in a 2013 paper (published in 2018). In order to understand further the genus g(L) of a regular language L, we introduce the genus size of |L|gen to be the minimal size of all finite deterministic automata of genus g(L) computing L.We show that the minimal finite deterministic automaton of a regular language can be arbitrarily far away from a finite deterministic automaton realizing the minimal genus and computing the same language, in terms of both the difference of genera and the difference in size. In particular, we show that the genus size |L|gen can grow at least exponentially in size |L|. We conjecture, however, the genus of every regular language to be computable. This conjecture implies in particular that the planarity of a regular language is decidable, a question asked in 1976 by R. V. Book and A. K. Chandra. We prove here the conjecture for a fairly generic class of regular languages having no short cycles. The methods developed for the proof are used to produce new genus-based hierarchies of regular languages and in particular, we show a new family of regular languages on a two-letter alphabet having arbitrary high genus.