Faceted browsing (also called faceted search or faceted navigation) is an exploratory search model where facets assist in the interactive navigation of search results. Facets are attributes that have been assigned to describe resources being explored; a faceted taxonomy is a collection of facets provided by the interface and is often organized as sets, hierarchies, or graphs. Faceted browsing has become ubiquitous with modern digital libraries and online search engines, yet the process is still difficult to abstractly model in a manner that supports the development of interoperable and reusable interfaces. We propose category theory as a theoretical foundation for faceted browsing and demonstrate how the interactive process can be mathematically abstracted in order to support the development of reusable and interoperable faceted systems. Existing efforts in facet modeling are based upon set theory, formal concept analysis, and light-weight ontologies, but in many regards they are implementations of faceted browsing rather than a specification of the basic, underlying structures and interactions. We will demonstrate that category theory allows us to specify faceted objects and study the relationships and interactions within a faceted browsing system. Resulting implementations can then be constructed through a category-theoretic lens using these models, allowing abstract comparison and communication that naturally support interoperability and reuse. In this context, reuse and interoperability are at two levels: between discrete systems and within a single system. Our model works at both levels by leveraging category theory as a common language for representation and computation. We will establish facets and faceted taxonomies as categories and will demonstrate how the computational elements of category theory, including products, merges, pushouts, and pullbacks, extend the usefulness of our model. More specifically, we demonstrate that categorical constructions such as the pullback and pushout operations can help organize and reorganize facets; these operations in particular can produce faceted views containing relationships not found in the original source taxonomy. We show how our category-theoretic model of facets relates to database schemas and discuss how this relationship assists in implementing the abstractions presented. We give examples of interactive interfaces from the biomedical domain to help illustrate how our abstractions relate to real-world requirements while enabling systematic reuse and interoperability. We introduce DELVE (Document ExpLoration and Visualization Engine), our framework for developing interactive visualizations as modular Web-applications in order to assist researchers with exploratory literature search. We show how facets relate to and control visualizations; we give three examples of text visualizations that either contain or interact with facets. We show how each of these visualizations can be represented with our model and demonstrate how our model directly informs implementation. With our general framework for communicating consistently about facets at a high level of abstraction, we enable the construction of interoperable interfaces and enable the intelligent reuse of both existing and future efforts.

Doctor of Philosophy / Department of Mathematics / Louis Crane / In this thesis we explore the possibilities of obtaining Topological Quantum Field Theories using cobordisms with corners to break further down in the structure of manifolds of a given dimension. The algebraic data obtained is described in the language of higher category theory, more precisely in its cubical approach which we explore here as well. Interesting connections are proposed to some important objects in Physics: the representations of the Poincaré group. Finally we will describe in great details the topological tools needed to describe the categories of cobordisms with corners and give some conjectures on their nature.

[pt] Considere os seguintes dois tipos de transformções em demonstrações: 1) tornar uma prova mais incompleta, apagando um lema ou uma construção que sejam parte da prova e pondo no lugar um aviso dizendo isso é óbvio; 2) pegar um passo que foi provado por um isso é óbvio, aplicar algum algoritmo que encontre uma demonstração para esse passo, e trocar o aviso pela demonstração de verdade. Nós vamos considerar que a primeira operação vai em direção ao esqueleto da demonstração, e que ela é como uma projeção; a segunda operação é um levantamento de um esqueleto para uma demonstração um pouco mais completa com aquele esqueleto. Nós só estamos interessados em esqueletos que possam ser levantados até provas completas usando algum algoritmo conhecido. Nesta tese descrevemos uma linguagem - o sistema DNC - que permite provar vários fatos sobre categorias usando esqueletos. O método para o levantamento é, a grosso modo, o seguinte: a partir do nome de um termo em DNC nós podemos obter o seu tipo; por uma espécie de Isomorfismo de Curry-Howard um tipo desses pode ser visto como uma preposição numa certa lógica; um algoritmo que obtenha uma demonstração para essa proposição retorna uma árvore de demonstração (uma derivação) num certo sistema de Dedução Natural, e essa árvore pode ser lida como um lambda- termo do tipo dado - ela dá uma construção natural para um objeto daquele tipo, e esse objeto muito frequentemente é exatamente o objeto que esperávamos obter. Derivações em DNC podem ser traduzidas para derivações num Pure Type System com Dicionários (PTSD), e derivações em PTSDs podem ser traduzidas para derivações em Pure Type Systems (PTSs); daí, questões sobre a teoria da prova de DNC se tornam questões sobre a teoria da prova de PTSs, que é bastante bem-conhecida. Não só temos um levantamento de nomes de termos em DNC para provas completas, mas também temos um modo formal de levantar diagramas categóricos expressos na linguagem do DNC para termos em DNC e daí para provas completas; e se mudamos o dicionário embutido num PTSD podemos fazer com que o mesmo esqueleto em DNC represente provas em contextos diferentes; por exemplo, algumas provas que aparentemente estão sendo feitas sobre a categoria dos conjuntos podem ser reinterpretados como provas sobre um topos arbitrário. Usamos essa idéia para apresentar de uma forma simples - em que os passos óbvios omitidos são óbvios num sentido muito preciso - a semântica categárica para alguns PTSs, incluindo PTSs com polimorfismo e tipos dependentes, e os PTSs para quais as derivações em DNC são traduzidas. / [en] Consider the following two kinds of transformation on proofs; the first is to make a a proof more incomplete, by erasing a lemma or a construction from it and replacing it by a tag saying this is obvious; the second kind of transformation takes a step that is proved by a this is obvious tag, applies some kind of prof-search algorithm to it, and replaces the tag by a real proof for that step. We will consider that the first operation goes toward the skeleton towards a more complete proof that had that skeleton as a projection. We are only interested in skeletons can be lifted back to full proofs using some known algorithm. In this thesis we can describe a language - DNC - that lets us prove several categorical facts using skeletons. The method for lifting these skeletons goes like this: from the name of a DNC term we can obtain its type; by a kind of Curry-Howard isomorphism a such type can be seen as a proposition in a certain logic; proof-search for that proposition will obtain a proof-tree for it in a certain system of Natural Deduction, and that proof-tree can be read as a lambda-term of given type - the proof-tree gives a natural construction for an object of the given type, that very often is exactly the object that we were looking for. Derivations in DNC can be translated into derivations in a Pure Type System with Dictionaries (PTSD), and derivations in PTSDs can be translated into derivations in Pure Type Systems (PTSs); so questions about the proof- theory of DNC become questions about the proof-theory of PTSs, whose properties are quite well-known. Also, not only we can lift names of terms in DNC to full proofs in different settings; for example, some proofs that apparently are happening over the category of sets can be reinterpreted as proofs over an arbitrary topos. We use that idea to give a simple presentation (in which the omitted obvious steps are obvious in a very precise sense) of the categorical semantics for some PTSs - and that includes PTSs into which the DNC derivations are translated.

In the 1980s and 1990s, Joyal and Street developed a graphical notation for various flavours of monoidal category using graphs drawn in the plane, commonly known as string diagrams. In particular, their work comprised a rigorous topological foundation of the notation. In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notions they called ⊸-schedules, ⊗-schedules and heaps. Schedules described interleavings of plays in games formed using ⊸ and ⊗, and heaps provided pointers used for backtracking. Their definitions were combinatorial in nature, but researchers often draw certain pictures when working in practice. In this thesis, we extend the framework of Joyal and Street to give a formal account of the graphical methods already informally employed by researchers in game semantics. We give a geometric formulation of ⊸-schedules and ⊗-schedules, and prove that the games they describe are isomorphic to those described in Harmer et al.’s terms, and also those given by a more general graphical representation of interleaving across games of multiple components. We further illustrate the value of the geometric methods by demonstrating that several proofs of key properties (such as that the composition of ⊸-schedules is associative) can be made straightforward, reflecting the geometry of the plane, and overstepping some of the cumbersome combinatorial detail of proofs in Harmer et al.’s terms. We further extend the framework of formal plane diagrams to account for the heaps and pointer structures used in the backtracking functors for O and P.

Este trabalho propõe o estudo dos espaços coerentes do ponto de vista da teoria dos topos, ou seja, consiste em uma análise, em termos de topos, das principais categorias de espaços coerentes. Os espaços coerentes constituem um tipo de domínio que apresenta algumas particularidades que o distinguem dos demais, por exemplo, considera admissíveis no conjunto de funções somente aquelas que, além de contínuas no sentido de Scott - preservam supremos de conjuntos dirigidos, também são estáveis e lineares. Um topos e uma categoria Cartesiana fechada com classificador de subobjetos. Isso faz com que todo topos se comporte como Set (conjuntos como objetos e funções como morfismos), ou seja, uma categoria na qual as interpretações de suas construções básicas seguem a Teoria dos Conjuntos. Entre as categorias de Espaços Coerentes, tem-se a categoria STAB, cujos objetos são os espaços coerentes e os morfismos são funções estáveis entre esses espaços, que é uma categoria cartesiana fechada. Isto significa que STAB é uma categoria especial no sentido computacional: além de possuir o produto binário para todos os seus objetos, STAB apresenta objeto exponencial e morfismo de avaliação, garantindo significado para processos computacionais. A subcategoria LIN da categoria STAB, cujos morfismos são as funções lineares, não é uma categoria cartesiana fechada. Entretanto, LIN é uma categoria monoidal simétrica que e fechada. Este, condição e suficiente para que em LIN também se tenha a garantia de se obter significado para processos computacionais. Apresenta-se então, uma interpretação computacional da estrutura destas categorias e uma análise das mesmas do ponto de vista de topos, isto é, da existência ou não de classificador de subobjetos. / This work proposes the study of coherent spaces from the point of view of the Topos Theory, that is, it consists of an analysis of the main categories of coherent spaces in terms of topos. The coherent spaces make up a kind of domain which presents some peculiarities that separate it from the rest, for example, in the complex whole of the functions it only considers permissible, those which, apart from being continuous in the sense of Scott - preserving supremo of directed sets, it is also stable and linear. A topos is a Cartesian closed with subobject classifier. This makes topos behaves like Set (sets as objects and functions as morphisms), that is, a category in which the interpretations of its basic constructions follow the Theory of Sets. Among the categories of Coherent Spaces, there is the STAB category, a closed Cartesian category, the objects of which are the coherent spaces, having morphisms as stable functions among these spaces. This means that STAB is a special category in the computational sense: apart from having a binary product for all its objects, STAB presents an exponential object and a morphism of evaluation, ensuring meaning for computational processes. The subcategory LIN of the STAB category, the morphisms of which are linear functions, is not a closed Cartesian category. However, LIN is a symmetrical monoidal category which is closed. This condition is sufficient to also have in LIN the guarantee of obtaining meaning for computational processes. Thus, a computational interpretation of the structure of these categories will be presented, as well as an analysis of them from the point of view of the Topos Theory, that is, if subobject classifier exists or not.

This thesis studies some constructions for building new models of Martin-Löf type theory out of old. We refer to the main techniques as gluing and idempotent splitting. For each we give general conditions under which type constructors exist in the resulting model. These techniques are used to construct some examples of Dialectica models of type theory. The name is chosen by analogy with de Paiva's Dialectica categories, which semantically embody Gödel's Dialectica functional interpretation and its variants. This continues a programme initiated by von Glehn with the construction of the polynomial model of type theory. We complete the analogy between this model and Gödel's original Dialectica by using our techniques to construct a two-level version of this model, equipping the original objects with an extra layer of predicates. In order to do this we have to carefully build up the theory of finite sum types in a display map category. We construct two other notable models. The first is a model analogous to the Diller-Nahm variant, which requires a detailed study of biproducts in categories of algebras. To make clear the generalization from the categories studied by de Paiva, we illustrate the construction of the Diller-Nahm category in terms of gluing an indexed system of types together with a system of predicates. Following this we develop the general techniques needed for the type-theoretic case. The second notable model is analogous to the Dialectica category associated to the error monad as studied by Biering. This model has only weak dependent products. In order to get a model with full dependent products we use the idempotent splitting construction, which generalizes the Karoubi envelope of a category. Making sense of the Karoubi envelope in the type-theoretic case requires us to face up to issues of coherence in our models. We choose the route of making sure all of the constructions we use preserve strict coherence, rather than applying a general coherence theorem to produce a strict model afterwards. Our chosen method preserves more detailed information in the final model.

Neste trabalho estabelecemos uma base teórica para a construção de uma teoria de rep- resentação de lógicas proposicionais. Iniciamos identificando uma relação precisa entre a categoria das lógicas (Blok-Pigozzi) algebrizáveis e a categoria de suas classes de álgebras associadas. Assim obtemos codificações funtoriais para as equipolências e morfismos den- sos entre lógicas. Na tentativa de generalizar os resultados obtidos sobre a codificação dos morfismos entre lógicas algebrizáveis, introduzimos a noção de funtor filtro e sua lógica asso- ciada. Classificamos alguns tipos especiais de lógicas e um estudo da propriedade metalógica de interpolação de Craig via amalgamação em matrizes para lógicas não-protoalgebrizáveis, e estabelecemos a relação entre a categoria dos funtores filtros e a categoria de lógicas. Em seguida, empregamos noções da teoria das instituições para definir instituições para as lógicas proposicionais abstratas, para uma lógica algebrizável e para uma lógica Lindenbaum alge- brizável. Sobre a instituição das lógicas algebrizáveis (lógicas Lindenbaum algebrizáveis), estabelecemos uma versão abstrata do Teorema de Glivenko e que é exatamente o tradi- cional teorema de Glivenko quando aplicado entre a lógica clássica e intuicionista. Por fim, influenciado pela teoria de representação para anéis, apresentamos os primeiros passos da teoria de representação de lógicas. Introduzimos as definições de diagramas modelos à esquerda para uma lógica, Morita equivalência e Morita equivalência estável para lógicas. Mostramos que quaisquer representações para lógica clássica são estavelmente Morita equiv- alentes, entretanto a lógica clássica e intuicionista não são estavelmente Morita equivalentes. / In this work we provide a framework in order to build a representation theory of proposi- tional logics. We begin identifying a precise relation between the category of (Blok-Pigozzi) algebraizable logic and the category of their classes of associated algebras. Then, we have a functorial codification for the equipollence and dense morphisms between logics. Attempt- ing generalize the results found before about codification of morphisms among algebraizable logics, we introduce the notion of filter functor and its associated logic. We classify some special kinds of logics and a study of a meta-logical Craig interpolation property via matri- ces amalgamation for non-protoalgebraizable logics, and we establish a relation between the category of filter functors and the category of logics. In the sequel, we employ notions of institution theory to define the institutions for the abstract propositional logics, for an al- gebraizable logic and Lindenbaum algebraizable logic. On the institutions for algebraizable logics (Lindenbaum algebraizable logics), we introduce the abstract Glivenkos theorem and this notion is exactly the traditional Glivenkos theorem when applied between the classical logic and intuitionistic logic. At last, influenced by the representation theory of rings, we present the first steps on the representation theory of logics. We introduce the definition of left diagram model for a logic, Morita equivalence of logics and stably-Morita equivalence for logics. We have showed that any presentation for classical logic are stably-Morita equivalent, but the classical logic and intuitionistic logic are not stably-Morita equivalent.

Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories.

<p>In this thesis we investigate two operational models of name-passing calculi: one based on coalgebra, and one based on enriched automata. We develop a semantic framework for modelling the open bisimulation in <i>π</i>-calculus, hyperbisimulation in Fusion calculus, and the first semantic interpretation of <i>FOλ</i>⁽<i>nabla</i>⁾ logic.</p><p>We consider a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of <i>atoms</i>. The key aspect of this model is to consider functors over the category of irreflexive and symmetric finite relations. The models previously proposed for the separate notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter.</p><p>Moreover, the new model admits a definition of <i>distinction-aware</i> simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu's <i>FOλ</i>⁽<i>nabla</i>⁾ logic. <i>FOλ</i>⁽<i>nabla</i>⁾ logic is designed for reasoning about operational semantics of languages with binding.</p><p>On the operational level, a contribution of the thesis is to extend an automata-based model for a variety of name-passing calculi with their associated notion of equivalence. HD-automata, a syntax-independent operational model, has been successfully applied for modelling e.g. early and late bisimulation in <i>π</i>-calculus and hyperbisimulation in Fusion calculus. However, current HD-automata are not adequate for modelling open bisimulation because they can not handle distinction-preserving substitutions. We solve this technical problem by integrating the notion of distinction into the definition of named sets, the basic building blocks of HD-automata. Finally, we discuss the relationship between HD-automata with distinctions, and <b>D</b>-LTS. </p>

We study three category-theoretic types in the context of functional query languages (typed lambda-calculi extended with additional operations for bulk data processing). The types we study are: / Engineering and Applied Sciences