SU\G(𝔸)/K·U
Sign Up for free Log In

Author Description

Login to generate an author description

Ask a Question About This Mathematician

Extracting verified decision procedures: DPLL and Resolution

2015-03-10
Ulrich Berger , Andrew D. Lawrence , Fredrik Nordvall Forsberg +1 more
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are … This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability. We use non-computational quantifiers to remove redundant computational content from the extracted program and translate it into Haskell to improve performance. We also prove the equivalence between the resolution proof system and the DPLL proof system with a bound on the size of the resulting resolution proof. This demonstrates that it is possible to capture quantitative information about the extracted program on the proof level. The formalization is carried out in the interactive proof assistant Minlog.
View PDF Chat

Quotient Inductive-Inductive Types

2018-01-01
Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more
View PDF Chat

A compositional treatment of iterated open games

2018-05-29
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up … Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra semantics for infinite games. In the course of this, we introduce a new operator on games to model the economic concept of subgame perfection.
View PDF Chat

Three equivalent ordinal notation systems in cubical Agda

2020-01-20
Fredrik Nordvall Forsberg , Chuangjie Xu , Neil Ghani
We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal … We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.
View PDF Chat

Translating Extensive Form Games to Open Games with Agency

2022-10-31
Matteo Capucci , Neil Ghani , Jérémy Ledent +1 more
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a … We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making progress towards a core, canonical and ergonomic calculus of game operators. Collectively these innovations increase the level of compositionality of open games, and demonstrate their expressiveness.
View PDF Chat

Positive Inductive-Recursive Definitions

2015-03-27
Neil Ghani , Fredrik Nordvall Forsberg , Lorenzo Malatesta
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive … A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.
View PDF Chat

Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law

2020-09-14
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games … We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games form a symmetric monoidal category, which can be used to compose probabilistic games in parallel and sequentially. We also consider morphisms between games, and show that intuitive constructions give rise to functors and adjunctions between pure and probabilistic open games.
View PDF Chat

Type-theoretic approaches to ordinals

2023-03-26
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
View PDF Chat

Positive Inductive-Recursive Definitions

2013-01-01
Neil Ghani , Lorenzo Malatesta , Fredrik Nordvall Forsberg
View PDF Chat

Compositional Game Theory, Compositionally

2021-01-19
Robert Atkey , Bruno Gavranović , Neil Ghani +3 more
We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new … We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new Arrows from old. We model equilibria as a bimodule over an Arrow and define an operator to build a new Arrow from such a bimodule over an existing Arrow. We also model strategies as graded Arrows and define an operator which builds a new Arrow by taking the colimit of a graded Arrow. A final operator builds a graded Arrow from a graded bimodule. We use this compositional approach to CGT to show how known and previously unknown variants of open games can be proven to form symmetric monoidal categories.
View PDF Chat

Catalog of Optimization Strategies and Realizations for Composed Integration Patterns

2019-01-01
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma +1 more
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of … The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of Enterprise Integration Patterns (EIPs), are only informally described, and thus their composition takes place in an informal, ad-hoc manner. This leads to several issues including a currently missing optimization of application integration scenarios. In this work, we collect and briefly explain the usage of process optimizations from the literature for integration scenario processes as catalog.

Set-Theoretic and Type-Theoretic Ordinals Coincide

2023-06-26
Tom de Jong , Nicolai Kraus , Fredrik Nordvall Forsberg +1 more
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We … In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
View PDF Chat

Connecting Constructive Notions of Ordinals in Homotopy Type Theory

2021-01-01
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We … In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.
View PDF Chat

Translating Extensive Form Games to Open Games with Agency

2021-01-01
Matteo Capucci , Neil Ghani , Jérémy Ledent +1 more
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a … We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making progress towards a core, canonical and ergonomic calculus of game operators. Collectively these innovations increase the level of compositionality of open games, and demonstrate their expressiveness.
View PDF Chat

A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists

2023-01-01
Clemens Kupke , Fredrik Nordvall Forsberg , Sean Watters

Higher inductive types in Homotopy Type Theory: applications and theory

2016-04-01
Fredrik Nordvall Forsberg

Catalog of Optimization Strategies and Realizations for Composed Integration Patterns.

2019-01-04
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma +1 more
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of … The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of Enterprise Integration Patterns (EIPs), are only informally described, and thus their composition takes place in an informal, ad-hoc manner. This leads to several issues including a currently missing optimization of application integration scenarios. In this work, we collect and briefly explain the usage of process optimizations from the literature for integration scenario processes as catalog.

Type-Theoretic Approaches to Ordinals

2022-01-01
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences … In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitely-branching trees); and third, extensional well-founded orders. Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and well-founded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional well-founded orders work well with infinite collections, but almost all properties are undecidable. Brouwer trees take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences. Our three approaches are connected by canonical order-preserving functions from the "more decidable" to the "less decidable" notions. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional well-founded orders have been studied and formalised thoroughly by Escardo and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger.
View PDF Chat

A Compositional Treatment of Iterated Open Games

2017-01-01
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up … Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra semantics for infinite games. In the course of this, we introduce a new operator on games to model the economic concept of subgame perfection.
View PDF Chat

Set-Theoretic and Type-Theoretic Ordinals Coincide

2023-01-01
Tom de Jong , Nicolai Kraus , Fredrik Nordvall Forsberg +1 more
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We … In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
View PDF Chat

Type-Theoretic Approaches to Ordinals

2023-02-20
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
View PDF Chat

Responsible Composition and Optimization of Integration Processes under Correctness Preserving Guarantees

2023-01-01
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma
Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scenarios. For integration scenarios, structurally correct composition of … Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scenarios. For integration scenarios, structurally correct composition of patterns into processes and improvements of integration processes are crucial. In order to achieve this, we formalize compositions of integration patterns based on their characteristics, and describe optimization strategies that help to reduce the model complexity, and improve the process execution efficiency using design time techniques. Using the formalism of timed DB-nets - a refinement of Petri nets - we model integration logic features such as control- and data flow, transactional data storage, compensation and exception handling, and time aspects that are present in reoccurring solutions as separate integration patterns. We then propose a realization of optimization strategies using graph rewriting, and prove that the optimizations we consider preserve both structural and functional correctness. We evaluate the improvements on a real-world catalog of pattern compositions, containing over 900 integration processes, and illustrate the correctness properties in case studies based on two of these processes.
View PDF Chat

Responsible composition and optimization of integration processes under correctness preserving guarantees

2024-04-30
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma
View PDF Chat

From Code to Compliance: Assessing ChatGPT's Utility in Designing an Accessible Webpage -- A Case Study

2025-01-07
Ammar Ahmed , Margarida Fresco , Fredrik Nordvall Forsberg +1 more
Web accessibility ensures that individuals with disabilities can access and interact with digital content without barriers, yet a significant majority of most used websites fail to meet accessibility standards. This … Web accessibility ensures that individuals with disabilities can access and interact with digital content without barriers, yet a significant majority of most used websites fail to meet accessibility standards. This study evaluates ChatGPT's (GPT-4o) ability to generate and improve web pages in line with Web Content Accessibility Guidelines (WCAG). While ChatGPT can effectively address accessibility issues when prompted, its default code often lacks compliance, reflecting limitations in its training data and prevailing inaccessible web practices. Automated and manual testing revealed strengths in resolving simple issues but challenges with complex tasks, requiring human oversight and additional iterations. Unlike prior studies, we incorporate manual evaluation, dynamic elements, and use the visual reasoning capability of ChatGPT along with the prompts to fix accessibility issues. Providing screenshots alongside prompts enhances the LLM's ability to address accessibility issues by allowing it to analyze surrounding components, such as determining appropriate contrast colors. We found that effective prompt engineering, such as providing concise, structured feedback and incorporating visual aids, significantly enhances ChatGPT's performance. These findings highlight the potential and limitations of large language models for accessible web development, offering practical guidance for developers to create more inclusive websites.
View PDF Chat

Ordinal Exponentiation in Homotopy Type Theory

2025-01-24
Tom de Jong , Nicolai Kraus , Fredrik Nordvall Forsberg +1 more
While ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus … While ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpi\'{n}ski based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
View PDF Chat

Ordinal Exponentiation in Homotopy Type Theory

2025-01-24
Tom de Jong , Nicolai Kraus , Fredrik Nordvall Forsberg +1 more
While ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus … While ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpi\'{n}ski based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
View PDF Chat

From Code to Compliance: Assessing ChatGPT's Utility in Designing an Accessible Webpage -- A Case Study

2025-01-07
Ammar Ahmed , Margarida Fresco , Fredrik Nordvall Forsberg +1 more
Web accessibility ensures that individuals with disabilities can access and interact with digital content without barriers, yet a significant majority of most used websites fail to meet accessibility standards. This … Web accessibility ensures that individuals with disabilities can access and interact with digital content without barriers, yet a significant majority of most used websites fail to meet accessibility standards. This study evaluates ChatGPT's (GPT-4o) ability to generate and improve web pages in line with Web Content Accessibility Guidelines (WCAG). While ChatGPT can effectively address accessibility issues when prompted, its default code often lacks compliance, reflecting limitations in its training data and prevailing inaccessible web practices. Automated and manual testing revealed strengths in resolving simple issues but challenges with complex tasks, requiring human oversight and additional iterations. Unlike prior studies, we incorporate manual evaluation, dynamic elements, and use the visual reasoning capability of ChatGPT along with the prompts to fix accessibility issues. Providing screenshots alongside prompts enhances the LLM's ability to address accessibility issues by allowing it to analyze surrounding components, such as determining appropriate contrast colors. We found that effective prompt engineering, such as providing concise, structured feedback and incorporating visual aids, significantly enhances ChatGPT's performance. These findings highlight the potential and limitations of large language models for accessible web development, offering practical guidance for developers to create more inclusive websites.
View PDF Chat

Responsible composition and optimization of integration processes under correctness preserving guarantees

2024-04-30
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma
View PDF Chat

Set-Theoretic and Type-Theoretic Ordinals Coincide

2023-06-26
Tom de Jong , Nicolai Kraus , Fredrik Nordvall Forsberg +1 more
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We … In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
View PDF Chat

Type-theoretic approaches to ordinals

2023-03-26
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
View PDF Chat

Type-Theoretic Approaches to Ordinals

2023-02-20
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
View PDF Chat

Set-Theoretic and Type-Theoretic Ordinals Coincide

2023-01-01
Tom de Jong , Nicolai Kraus , Fredrik Nordvall Forsberg +1 more
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We … In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
View PDF Chat

Responsible Composition and Optimization of Integration Processes under Correctness Preserving Guarantees

2023-01-01
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma
Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scenarios. For integration scenarios, structurally correct composition of … Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scenarios. For integration scenarios, structurally correct composition of patterns into processes and improvements of integration processes are crucial. In order to achieve this, we formalize compositions of integration patterns based on their characteristics, and describe optimization strategies that help to reduce the model complexity, and improve the process execution efficiency using design time techniques. Using the formalism of timed DB-nets - a refinement of Petri nets - we model integration logic features such as control- and data flow, transactional data storage, compensation and exception handling, and time aspects that are present in reoccurring solutions as separate integration patterns. We then propose a realization of optimization strategies using graph rewriting, and prove that the optimizations we consider preserve both structural and functional correctness. We evaluate the improvements on a real-world catalog of pattern compositions, containing over 900 integration processes, and illustrate the correctness properties in case studies based on two of these processes.
View PDF Chat

A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists

2023-01-01
Clemens Kupke , Fredrik Nordvall Forsberg , Sean Watters

Translating Extensive Form Games to Open Games with Agency

2022-10-31
Matteo Capucci , Neil Ghani , Jérémy Ledent +1 more
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a … We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making progress towards a core, canonical and ergonomic calculus of game operators. Collectively these innovations increase the level of compositionality of open games, and demonstrate their expressiveness.
View PDF Chat

Type-Theoretic Approaches to Ordinals

2022-01-01
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences … In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitely-branching trees); and third, extensional well-founded orders. Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and well-founded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional well-founded orders work well with infinite collections, but almost all properties are undecidable. Brouwer trees take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences. Our three approaches are connected by canonical order-preserving functions from the "more decidable" to the "less decidable" notions. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional well-founded orders have been studied and formalised thoroughly by Escardo and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger.
View PDF Chat

Compositional Game Theory, Compositionally

2021-01-19
Robert Atkey , Bruno Gavranović , Neil Ghani +3 more
We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new … We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new Arrows from old. We model equilibria as a bimodule over an Arrow and define an operator to build a new Arrow from such a bimodule over an existing Arrow. We also model strategies as graded Arrows and define an operator which builds a new Arrow by taking the colimit of a graded Arrow. A final operator builds a graded Arrow from a graded bimodule. We use this compositional approach to CGT to show how known and previously unknown variants of open games can be proven to form symmetric monoidal categories.
View PDF Chat

Connecting Constructive Notions of Ordinals in Homotopy Type Theory

2021-01-01
Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We … In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.
View PDF Chat

Translating Extensive Form Games to Open Games with Agency

2021-01-01
Matteo Capucci , Neil Ghani , Jérémy Ledent +1 more
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a … We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making progress towards a core, canonical and ergonomic calculus of game operators. Collectively these innovations increase the level of compositionality of open games, and demonstrate their expressiveness.
View PDF Chat

Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law

2020-09-14
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games … We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games form a symmetric monoidal category, which can be used to compose probabilistic games in parallel and sequentially. We also consider morphisms between games, and show that intuitive constructions give rise to functors and adjunctions between pure and probabilistic open games.
View PDF Chat

Three equivalent ordinal notation systems in cubical Agda

2020-01-20
Fredrik Nordvall Forsberg , Chuangjie Xu , Neil Ghani
We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal … We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.
View PDF Chat

Catalog of Optimization Strategies and Realizations for Composed Integration Patterns.

2019-01-04
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma +1 more
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of … The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of Enterprise Integration Patterns (EIPs), are only informally described, and thus their composition takes place in an informal, ad-hoc manner. This leads to several issues including a currently missing optimization of application integration scenarios. In this work, we collect and briefly explain the usage of process optimizations from the literature for integration scenario processes as catalog.

Catalog of Optimization Strategies and Realizations for Composed Integration Patterns

2019-01-01
Daniel Ritter , Fredrik Nordvall Forsberg , Stefanie Rinderle‐Ma +1 more
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of … The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of Enterprise Integration Patterns (EIPs), are only informally described, and thus their composition takes place in an informal, ad-hoc manner. This leads to several issues including a currently missing optimization of application integration scenarios. In this work, we collect and briefly explain the usage of process optimizations from the literature for integration scenario processes as catalog.

A compositional treatment of iterated open games

2018-05-29
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up … Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra semantics for infinite games. In the course of this, we introduce a new operator on games to model the economic concept of subgame perfection.
View PDF Chat

Quotient Inductive-Inductive Types

2018-01-01
Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more
View PDF Chat

A Compositional Treatment of Iterated Open Games

2017-01-01
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up … Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra semantics for infinite games. In the course of this, we introduce a new operator on games to model the economic concept of subgame perfection.
View PDF Chat

Higher inductive types in Homotopy Type Theory: applications and theory

2016-04-01
Fredrik Nordvall Forsberg

Positive Inductive-Recursive Definitions

2015-03-27
Neil Ghani , Fredrik Nordvall Forsberg , Lorenzo Malatesta
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive … A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.
View PDF Chat

Extracting verified decision procedures: DPLL and Resolution

2015-03-10
Ulrich Berger , Andrew D. Lawrence , Fredrik Nordvall Forsberg +1 more
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are … This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability. We use non-computational quantifiers to remove redundant computational content from the extracted program and translate it into Haskell to improve performance. We also prove the equivalence between the resolution proof system and the DPLL proof system with a bound on the size of the resulting resolution proof. This demonstrates that it is possible to capture quantitative information about the extracted program on the proof level. The formalization is carried out in the interactive proof assistant Minlog.
View PDF Chat

Positive Inductive-Recursive Definitions

2013-01-01
Neil Ghani , Lorenzo Malatesta , Fredrik Nordvall Forsberg
View PDF Chat
Coauthor Papers Together
Neil Ghani 9
Nicolai Kraus 8
Clemens Kupke 5
Chuangjie Xu 5
Daniel Ritter 4
Stefanie Rinderle‐Ma 4
Chuangjie Xu 3
Tom de Jong 3
Jérémy Ledent 3
Alasdair Lambert 3
Matteo Capucci 2
Lorenzo Malatesta 2
Margarida Fresco 1
Ulrich Berger 1
Hallvard Grotli 1
Gabe Dijkstra 1
Paolo Capriotti 1
Robert Atkey 1
Norman May 1
Bruno Gavranović 1
Monika Seisenberger 1
Thorsten Altenkirch 1
Ammar Ahmed 1
Sean Watters 1
Andrew D. Lawrence 1
Norman May 1

Semantics of higher inductive types

2019-06-17
Peter LeFanu Lumsdaine , Michael Shulman
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development … Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.
View PDF Chat

Compositional Game Theory

2018-06-27
Neil Ghani , Jules Hedges , Viktor Winschel +1 more
We introduce open games as a compositional foundation of economic game theory. A compositional approach potentially allows methods of game theory and theoretical computer science to be applied to large-scale … We introduce open games as a compositional foundation of economic game theory. A compositional approach potentially allows methods of game theory and theoretical computer science to be applied to large-scale economic models for which standard economic tools are not practical. An open game represents a game played relative to an arbitrary environment and to this end we introduce the concept of coutility, which is the utility generated by an open game and returned to its environment. Open games are the morphisms of a symmetric monoidal category and can therefore be composed by categorical composition into sequential move games and by monoidal products into simultaneous move games. Open games can be represented by string diagrams which provide an intuitive but formal visualisation of the information flows. We show that a variety of games can be faithfully represented as open games in the sense of having the same Nash equilibria and off-equilibrium best responses.
View PDF Chat

A compositional treatment of iterated open games

2018-05-29
Neil Ghani , Clemens Kupke , Alasdair Lambert +1 more
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up … Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra semantics for infinite games. In the course of this, we introduce a new operator on games to model the economic concept of subgame perfection.
View PDF Chat

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01
Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
View PDF Chat

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-01
Daniel R. Licata , Michael Shulman
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new … Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.
View PDF Chat

Continuous increasing functions of finite and transfinite ordinals

1908-01-01
Oswald Veblen
View PDF Chat

The many faces of data-centric workflow optimization: a survey

2018-03-06
Georgia Kougka , Anastasios Gounaris , Alkis Simitsis
View PDF Chat

Perfect trees and bit-reversal permutations

2000-05-01
Ralf Hinze
One well known algorithm is the Fast Fourier Transform (FFT). An efficient iterative version of the FFT algorithm performs as a first step a bit-reversal permutation of the input list. … One well known algorithm is the Fast Fourier Transform (FFT). An efficient iterative version of the FFT algorithm performs as a first step a bit-reversal permutation of the input list. The bit-reversal permutation swaps elements whose indices have binary representations that are the reverse of each other. Using an amortized approach, this operation can be made to run in linear time on a random-access machine. An intriguing question is whether a linear-time implementation is also feasible on a pointer machine, that is, in a purely functional setting. We show that the answer to this question is in the affirmative. In deriving a solution, we employ several advanced programming language concepts such as nested datatypes, associated fold and unfold operators, rank-2 types and polymorphic recursion.
View PDF Chat

Quotient Inductive-Inductive Types

2018-01-01
Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more
View PDF Chat

Connected limits, familial representability and Artin glueing

1995-12-01
A. Carboni , Peter Johnstone
We consider the following two properties of a functor F from a presheaf topos to the category of sets: (a) F preserves connected limits, and (b) the Artin glueing of … We consider the following two properties of a functor F from a presheaf topos to the category of sets: (a) F preserves connected limits, and (b) the Artin glueing of F is again a presheaf topos. We show that these two properties are in fact equivalent. In the process, we develop a general technique for associating categorical properties of a category obtained by Artin glueing with preservation properties of the functor along which the glueing takes place. We also give a syntactic characterization of those monads on Set whose functor parts have the above properties, and whose units and multiplications are cartesian natural transformations.

A new system of proof-theoretic ordinal functions

1986-01-01
Wilfried Buchholz
View PDF Chat

An intuitionistic theory of types

1998-10-15
Per Martin-Löf
The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by … The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by Bishop 1967. The language of the theory is richer than the language of first order predicate logic. This makes it possible to strengthen the axioms for existence and disjunction. In the case of existence, the possibility of strengthening the usual elimination rule seems first to have been indicated by Howard 1969, whose proposed axioms are special cases of the existential elimination rule of the present theory. Furthermore, there is a reflection principle which links the generation of objects and types and plays somewhat the same role for the present theory as does the replacement axiom for Zermelo-Fraenkel set theory. An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis. Mathematical objects and their types. We shall think of mathematical objects or constructions. Every mathematical object is of a certain kind or type. Better, a mathematical object is always given together with its type, that is, it is not just an object, it is an object of a certain type.

Partiality, Revisited

2017-01-01
Thorsten Altenkirch , Nils Anders Danielsson , Nicolai Kraus
View PDF Chat

Una questione sui numeri transfiniti

1897-12-01
C. Burali-Forti
View PDF Chat

On Higher Inductive Types in Cubical Type Theory

2018-06-27
Thierry Coquand , Simon Huber , Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
View PDF Chat

Backprop as Functor: A compositional perspective on supervised learning

2019-06-01
Brendan Fong , David I. Spivak , Rémy Tuyéras
A supervised learning algorithm searches over a set of functions <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$A\rightarrow B$</tex> parametrised by a space <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$P$</tex> to find the best approximation to some ideal function … A supervised learning algorithm searches over a set of functions <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$A\rightarrow B$</tex> parametrised by a space <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$P$</tex> to find the best approximation to some ideal function <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$f:A\rightarrow B$</tex> . It does this by taking examples <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(a, f(a))\in A\times B$</tex> , and updating the parameter according to some rule. We define a category where these update rules may be composed, and show that gradient descent-with respect to a fixed step size and an error function satisfying a certain property-defines a monoidal functor from a category of parametrised functions to this category of update rules. A key contribution is the notion of request function. This provides a structural perspective on backpropagation, giving a broad generalisation of neural networks and linking it with structures from bidirectional programming and open games.
View PDF Chat

Positive Inductive-Recursive Definitions

2015-03-27
Neil Ghani , Fredrik Nordvall Forsberg , Lorenzo Malatesta
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -&gt; Fam(C) is presented. This theory, which we call positive … A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -&gt; Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.
View PDF Chat

Eilenberg-MacLane spaces in homotopy type theory

2014-07-14
Daniel R. Licata , Eric Finster
Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs … Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group G, an Eilenberg-MacLane space K(G,n) is a space (type) whose nth homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in G. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.
View PDF Chat

Lexicographic exponentiation of chains

2005-06-01
W. Charles Holland , Salma Kuhlmann , Stephen H. McCleary
Abstract The lexicographic power Δ Γ of chains Δ and Γ is, roughly, the Cartesian power Π γЄΓ Δ totally ordered lexicographically from the left. Here the focus is on … Abstract The lexicographic power Δ Γ of chains Δ and Γ is, roughly, the Cartesian power Π γЄΓ Δ totally ordered lexicographically from the left. Here the focus is on certain powers in which either Δ = ℝ or ℚ = ℝ, with emphasis on when two such powers are isomorphic and on when Δ Γ is 2-homogeneous. The main results are: (1) For a countably infinite ordinal (2) ℝ ℝ ≄ ℝ ℚ . (3) For Δ a countable ordinal ≥ 2, Δ ℝ with its smallest element deleted, is 2-homogeneous.

A Categorical Programming Language

2020-01-01
Tatsuya Hagino
A theory of data types based on category theory is presented. We organize data types under a new categorical notion of F,G-dialgebras which is an extension of the notion of … A theory of data types based on category theory is presented. We organize data types under a new categorical notion of F,G-dialgebras which is an extension of the notion of adjunctions as well as that of T-algebras. T-algebras are also used in domain theory, but while domain theory needs some primitive data types, like products, to start with, we do not need any. Products, coproducts and exponentiations (i.e. function spaces) are defined exactly like in category theory using adjunctions. F,G-dialgebras also enable us to define the natural number object, the object for finite lists and other familiar data types in programming. Furthermore, their symmetry allows us to have the dual of the natural number object and the object for infinite lists (or lazy lists). We also introduce a programming language in a categorical style using F,G-dialgebras as its data type declaration mechanism. We define the meaning of the language operationally and prove that any program terminates using Tait's computability method.

From coinductive proofs to exact real arithmetic: theory and applications

2011-03-24
Ulrich Berger
Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number … Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.
View PDF Chat

Constructing the propositional truncation using non-recursive HITs

2016-01-12
Floris van Doorn
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive … In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.
View PDF Chat

Familial 2-functors and parametric right adjoints

2007-01-01
Mark Weber
We define and study familial 2-functors primarily with a view to the devel- opment of the 2-categorical approach to operads of (Weber, 2005). Also included in this paper is a … We define and study familial 2-functors primarily with a view to the devel- opment of the 2-categorical approach to operads of (Weber, 2005). Also included in this paper is a result in which the well-known characterisation of a category as a simplicial set via the Segal condition, is generalised to a result about nice monads on cocomplete categories. Instances of this general result can be found in (Leinster, 2004), (Berger, 2002) and (Moerdijk-Weiss, 2007b). Aspects of this general theory are then used to show that the composite 2-monads of (Weber, 2005) that describe symmetric and braided ana- logues of the !-operads of (Batanin, 1998), are cartesian 2-monads and their underlying endo-2-functor is familial. Intricately linked to the notion of familial 2-functor is the theory of fibrations in a finitely complete 2-category (Street, 1974) (Street, 1980a), and those aspects of that theory that we require, that weren't discussed in (Weber, 2007), are reviewed here.

Extending Homotopy Type Theory with Strict Equality

2016-04-13
Thorsten Altenkirch , Paolo Capriotti , Nicolai Kraus
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of … In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an one, containing a strict equality type former, and an one, which is some version of HoTT. Our type theory is inspired by Voevosky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we no not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of infinite structures which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with schematic definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.

A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory

2016-01-01
Kuen-Bang Hou , Eric Finster , Daniel R. Licata +1 more
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the … This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations. The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.
View PDF Chat

Doubles for monoidal categories: Dedicated to Walter Tholen on his 60th birthday

2008-06-06
Craig Pastro , Ross Street
In a recent paper, Daisuke Tambara defined two-sided actions on an en- domodule (= endodistributor) of a monoidal V -category A. When A is autonomous (= rigid = compact), he … In a recent paper, Daisuke Tambara defined two-sided actions on an en- domodule (= endodistributor) of a monoidal V -category A. When A is autonomous (= rigid = compact), he showed that the V -category (that we call Tamb(A )) of so- equipped endomodules (that we call Tambara modules) is equivalent to the monoidal centre Z(A ,V ) of the convolution monoidal V -category (A ,V ). Our paper extends these ideas somewhat. For general A , we construct a promonoidal V -category DA (which we suggest should be called the double of A ) with an equivalence (DA ,V ) ' Tamb(A ). When A is closed, we define strong (respectively, left strong) Tambara modules and show that these constitute a V -category Tambs(A ) (respectively, Tambls(A )) which is equivalent to the centre (respectively, lax centre) of (A ,V ). We construct localizations DsA and DlsA of DA such that there are equivalences Tambs(A ) ' (DsA ,V ) and Tambls(A ) ' (DlsA ,V ). When A is autonomous, every Tambara module is strong; this implies an equivalence Z(A ,V ) ' (DA ,V ).

Constructions with Non-Recursive Higher Inductive Types

2016-07-05
Nicolai Kraus
Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to … Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs.
View PDF Chat

On the homotopy groups of spheres in homotopy type theory

2016-06-15
Guillaume Brunerie
The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the … The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12
Chris Kapulkin , Peter LeFanu Lumsdaine
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

Proof Theory in Computer Science

2001-01-01
Reinhard Kähle , Peter Schroeder‐Heister , Robert F. Stärk
View PDF Chat

Multisets in type theory

2019-03-27
Håkon Robbestad Gylterud
A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a … A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin-L\"of Type Theory, in the presence of Voevodsky's Univalence Axiom. Aczel 1978 introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the Univalence Axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.
View PDF Chat

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type

2016-10-28
Thorsten Altenkirch , Nils Anders Danielsson , Nicolai Kraus
Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by … Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.
View PDF Chat

Cubical Type Theory: a constructive interpretation of the univalence axiom

2015-05-18
Cyril Cohen , Thierry Coquand , Simon Huber +1 more
This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in … This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
View PDF Chat

DB-Nets: On the Marriage of Colored Petri Nets and Relational Databases

2017-01-01
Marco Montali , Andrey Rivkin
View PDF Chat

The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)

2014-01-01
Vladimir Voevodsky
This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). … This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). The first presentation of the axiom was in a lecture at LMU Munich in November 2009.

Homotopy Type Theory: The Logic of Space

2021-03-22
Michael Shulman
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces … This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).
View PDF Chat

The real projective spaces in homotopy type theory

2017-06-01
Ulrik Buchholtz , Egbert Rijke
Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about … Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> , as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">-1</sup> to be the empty type. In the inductive step, we take ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n+1</sup> to be the mapping cone of the projection map of the tautological bundle of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> , and we use its universal property and the univalence axiom to define the tautological bundle on ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n+1</sup> . By showing that the total space of the tautological bundle of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> is the n-sphere S <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> , we retrieve the classical description of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n+1</sup> as ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> with an (n + 1)-disk attached to it. The infinite dimensional real projective space ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">∞</sup> , defined as the sequential colimit of ℝP <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</sup> with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(ℤ/2ℤ, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.
View PDF Chat

Finite sets in homotopy type theory

2018-01-08
Dan Frumin , Herman Geuvers , Léon Gondelman +1 more
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
View PDF Chat

Backward Induction for Repeated Games

2018-07-10
Jules Hedges
We present a method of backward induction for computing approximate subgame perfect Nash equilibria of infinitely repeated games with discounted payoffs. This uses the selection monad transformer, combined with the … We present a method of backward induction for computing approximate subgame perfect Nash equilibria of infinitely repeated games with discounted payoffs. This uses the selection monad transformer, combined with the searchable set monad viewed as a notion of 'topologically compact' nondeterminism, and a simple model of computable real numbers. This is the first application of Escard\'o and Oliva's theory of higher-order sequential games to games of imperfect information, in which (as well as its mathematical elegance) lazy evaluation does nontrivial work for us compared with a traditional game-theoretic analysis. Since a full theoretical understanding of this method is lacking (and appears to be very hard), we consider this an 'experimental' paper heavily inspired by theoretical ideas. We use the famous Iterated Prisoner's Dilemma as a worked example.
View PDF Chat

Finitary Higher Inductive Types in the Groupoid Model

2018-04-01
Peter Dybjer , Hugo Moeneclaey
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces … A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.
View PDF Chat

What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)

2018-07-30
Guillaume Boisseau , Jeremy Gibbons
Profunctor optics are a neat and composable representation of bidirectional data accessors, including lenses, and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes, but … Profunctor optics are a neat and composable representation of bidirectional data accessors, including lenses, and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes, but the relationship between this and the familiar representation in terms of "getter" and "setter" functions is not at all obvious. We derive the profunctor representation from the concrete representation, making the relationship clear. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory. We hope this derivation aids understanding of the profunctor representation. Conversely, it might also serve to provide some insight into the Yoneda Lemma.
View PDF Chat

Categories of Optics

2018-09-03
Mitchell Riley
Bidirectional data accessors such as lenses, prisms and traversals are all instances of the same general 'optic' construction. We give a careful account of this construction and show that it … Bidirectional data accessors such as lenses, prisms and traversals are all instances of the same general 'optic' construction. We give a careful account of this construction and show that it extends to a functor from the category of symmetric monoidal categories to itself. We also show that this construction enjoys a universal property: it freely adds counit morphisms to a symmetric monoidal category. Missing in the folklore is a general definition of 'lawfulness' that applies directly to any optic category. We provide such a definition and show that it is equivalent to the folklore profunctor optic laws.

Don't Try This at Home: No-Go Theorems for Distributive Laws

2018-01-01
Dan Marsden
Beck's distributive laws provide sufficient conditions under which two monads can be composed, and monads arising from distributive laws have many desirable theoretical properties. Unfortunately, finding and verifying distributive laws, … Beck's distributive laws provide sufficient conditions under which two monads can be composed, and monads arising from distributive laws have many desirable theoretical properties. Unfortunately, finding and verifying distributive laws, or establishing if one even exists, can be extremely difficult and error-prone. We develop general-purpose techniques for showing when there can be no distributive law between two monads. Two approaches are presented. The first widely generalizes ideas from a counterexample attributed to Plotkin, yielding general-purpose theorems that recover the previously known situations in which no distributive law can exist. Our second approach is entirely novel, encompassing new practical situations beyond our generalization of Plotkin's approach. It negatively resolves the open question of whether the list monad distributes over itself. Our approach adopts an algebraic perspective throughout, exploiting a syntactic characterization of distributive laws. This approach is key to generalizing beyond what has been achieved by direct calculations in previous work. We show via examples many situations in which our theorems can be applied. This includes a detailed analysis of distributive laws for members of an extension of the Boom type hierarchy, well known to functional programmers.

Positive Inductive-Recursive Definitions

2013-01-01
Neil Ghani , Lorenzo Malatesta , Fredrik Nordvall Forsberg
View PDF Chat

Signatures and Induction Principles for Higher Inductive-Inductive Types

2019-01-01
Ambrus Kaposi , András Kovács
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed … Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
View PDF Chat

Notions of computation as monoids

2017-01-01
Exequiel Rivas , Mauro Jaskelioff
Abstract There are different notions of computation, the most popular being monads, applicative functors, and arrows. In this article, we show that these three notions can be seen as instances … Abstract There are different notions of computation, the most popular being monads, applicative functors, and arrows. In this article, we show that these three notions can be seen as instances of a unifying abstract concept: monoids in monoidal categories. We demonstrate that even when working at this high level of generality, one can obtain useful results. In particular, we give conditions under which one can obtain free monoids and Cayley representations at the level of monoidal categories, and we show that their concretisation results in useful constructions for monads, applicative functors, and arrows. Moreover, by taking advantage of the uniform presentation of the three notions of computation, we introduce a principled approach to the analysis of the relation between them.
View PDF Chat

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

2016-07-05
Kuen-Bang Hou , Eric Finster , Daniel R. Licata +1 more
This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result … This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.
View PDF Chat

FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY

2018-09-01
Håkon Robbestad Gylterud
We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can … We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-Löf type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel's 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of "Homotopy Type Theory" by the Univalent Foundations Program.
View PDF Chat

A constructive interpretation of Ramsey's theorem via the product of selection functions

2014-11-13
Paulo Oliva , Thomas Powell
We use Gödel's dialectica interpretation to produce a computational version of the well-known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection … We use Gödel's dialectica interpretation to produce a computational version of the well-known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
View PDF Chat

No-Go Theorems for Distributive Laws

2019-06-01
Maaike Zwart , Dan Marsden
Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some principles for … Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some principles for constructing distributive laws. However, until now there have been no general techniques for establishing when no such law exists. We present two families of theorems for showing when there can be no distributive law for two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second family is entirely novel, encompassing various new practical situations. For example, it negatively resolves the open question of whether the list monad distributes over itself, and also reveals a previously unobserved error in the literature.
View PDF Chat