258 research outputs found
Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor
No full textThe finite powerset functor is a construct frequently employed for the specification of nondeterministic transition systems as coalgebras. The final coalgebra of the finite powerset functor, whose elements characterize the dynamical behavior of transition systems, is a well-understood object which enjoys many equivalent presentations in set-theoretic foundations based on classical logic.
In this paper, we discuss various constructions of the final coalgebra of the finite powerset functor in constructive type theory, and we formalize our results in the Cubical Agda proof assistant. Using setoids, the final coalgebra of the finite powerset functor can be defined from the final coalgebra of the list functor. Using types instead of setoids, as it is common in homotopy type theory, one can specify the finite powerset datatype as a higher inductive type and define its final coalgebra as a coinductive type. Another construction is obtained by quotienting the final coalgebra of the list functor, but the proof of finality requires the assumption of the axiom of choice. We conclude the paper with an analysis of a classical construction by James Worrell, and show that its adaptation to our constructive setting requires the presence of classical axioms such as countable choice and the lesser limited principle of omniscience
Data Types with Symmetries via Action Containers
No full textWe study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids.
Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction
Constructive Final Semantics of Finite Bags
No full textFinitely-branching and unlabelled dynamical systems are typically modelled as coalgebras for the finite powerset functor. If states are reachable in multiple ways, coalgebras for the finite bag functor provide a more faithful representation. The final coalgebra of this functor is employed as a denotational domain for the evaluation of such systems. Elements of the final coalgebra are non-wellfounded trees with finite unordered branching, representing the evolution of systems starting from a given initial state.
This paper is dedicated to the construction of the final coalgebra of the finite bag functor in homotopy type theory (HoTT). We first compare various equivalent definitions of finite bags employing higher inductive types, both as sets and as groupoids (in the sense of HoTT). We then analyze a few well-known, classical set-theoretic constructions of final coalgebras in our constructive setting. We show that, in the case of set-based definitions of finite bags, some constructions are intrinsically classical, in the sense that they are equivalent to some weak form of excluded middle. Nevertheless, a type satisfying the universal property of the final coalgebra can be constructed in HoTT employing the groupoid-based definition of finite bags. We conclude by discussing generalizations of our constructions to the wider class of analytic functors
Guarded Recursion in Agda via Sized Types
No full textIn type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator
Co władca powinien wiedzieć o władaniu – według egipskich mędrców i Niccolò Machiavellego
No full textThe paper studies the thought of Ancient Egypt in the context of Niccolò Machiavelli’s work entitled The Prince, which has not yet been examined in the context of political philosophy. The author outlines many similarities between the texts and their authors’ honest and substantive approach to the subject discussed. It seems that through the realistic presentation of selected aspects of power, these works are practical guides for the authorities rather than only postulates regarding the functioning of the state and the ruler. At the same time, the author of the article seeks to stress the value of these works which express the political thought of their time and contain some universal observations
Recepcja pism Niccolò Machiavellego w twórczości literackiej Andrzeja Maksymiliana Fredry
No full textIn this article I will try to show to what extent the writings of Niccolò Machiavelli influenced the literary work of Andrzej Maksymilian Fredro. It is worth mentioning that the political thought of the author of The Prince was widely known among the Polish intellectual elite in the 17th century. However, in the old Poland, the Florentine was increasingly criticized, as he was believed to promote a type of politics full of falsehood and cynicism. In his works, Fredro did not perceive Machiavelli in this way. He was referring to the ideas contained in two works – different in content – by the Florentine secretary: The Prince and Discourses on the First Decade of Titus Livius.W niniejszym artykule postaram się ukazać, w jakim stopniu pisma Niccolò Machiavellego oddziaływały na twórczość literacką Andrzeja Maksymiliana Fredry. Warto wspomnieć, że myśl polityczna autora Księcia była w XVII w. rozpowszechniona wśród polskiej elity umysłowej. Jednak w dawnej Polsce coraz częściej krytykowano Florentczyka, uważając, iż propaguje typ polityki przepełnionej fałszem i cynizmem. Fredro w swoich dziełach nie postrzegał w ten sposób Machiavellego. Odnosił się bowiem do idei zawartych w dwóch – różnych pod względem treści – dziełach florenckiego sekretarza: Księciu oraz Rozważaniach nad pierwszym dziesięcioksięgiem historii Rzymu Liwiusza
In Praise For Monstrosities. The Case of Niccolò Machiavelli
No full textIn the paper author refers to the passage from The Prince of Niccolò Machiavelli, in which the famous Florentine says that there are two kinds of combat: one with laws, the other with force. Author defend the claim that by writing this, Machiavelli opened up a new and still unused way of thinking about nature-culture relationship. A follower of this way of thinking withdraws from saying that nature is surpassed by culture, or that nature is nothing else but a subject of an on-going human speculation, and rebuts the sole hypothesis that what there is, is nothing but nature. Modern Western culture entrusted its key opposition to the nature-culture relationship. By and large, political philosophy is a story about surpassing the nature in order to establish a state under the rule of law. According to Machiavelli, the juxtaposition of nature and culture, the narrative on surpassing by politics the laws of nature, just as well as the narrative on us being stuck in it, are all utterly wrong. Accepting the ambiguity of the opposition between nature and culture and assuming that the social contract is indeed fictitious, author would like to question Machiavelli about his vision of subjectivity and politics in a world where “natural objects” appear to be socialized, and “cultural subjects” appear to be dissocial. In the way author puts the question: does Machiavelli recommend monstrosity by writing stories in praise of monstrosity as it may well seem
Per un'edizione delle postille di Niccolò Tommaseo alla Crusca veronese del Cesari
No full textThis article examines the handwritten annotations made by Niccolò Tommaseo in the first volume of the Crusca veronese edited by Abbot Antonio Cesari. It retraces the research process carried out by the author, with particular attention to the transcription and analysis of these annotations, aiming to reconstruct the Dalmatian scholar's linguistic reflections and lexicographic methods. The study highlights the systematic nature of Tommaseo's annotations and connects them to his later lexicographic works, such as the Nuovo dizionario de' sinonimi and the Dizionario della lingua italiana. Finally, the article presents a sample critical edition of selected annotations, accompanied by a discussion of the editorial criteria applied
Minimal session types for the €-calculus
No full textSession types enable the static verification of message-passing programs. A session type specifies a channel's protocol as sequences of messages. Prior work established a minimality result: every process typable with standard session types can be compiled down to a process typable using minimal session types: session types without the sequencing construct. This result justifies session types in terms of themselves; it holds for a higher-order session €-calculus, where values are abstractions (functions from names to processes). This paper establishes a new minimality result but now for the session €-calculus, the language in which values are names and for which session types have been more widely studied. Remarkably, this new minimality result can be obtained by composing known results. We develop optimizations of our new minimality result, and establish its static and dynamic correctness
En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
No full textReversible computation studies computations which exhibit both forward and backward determinism. Among others, it has been studied for half a century for its applications in low-power computing, and forms the basis for quantum computing. Though certified program equivalence is useful for a number of applications (e.g., certified compilation and optimization), little work on this topic has been carried out for reversible programming languages. As a notable exception, Carette and Sabry have studied the equivalences of the finitary fragment of a reversible combinator calculus, yielding a two-level calculus of type isomorphisms and equivalences between them. In this paper, we extend the two-level calculus of finitary to one for full (i.e., with both recursive types and iteration by means of a trace combinator) using the delay monad, which can be regarded as a “computability-aware” analogue of the usual maybe monad for partiality. This yields a calculus of iterative (and possibly non-terminating) reversible programs acting on user-defined dynamic data structures together with a calculus of certified program equivalences between these programs.</p
- …
