SPEAKER:
Yoshiki
Kobasigawa
(Department of Philosophy, University of Calgary)
Why the New Meinongian Analysis is Preferable to any Fregean Analysis
ABSTRACT: It is possible to identify three types of views that can be taken with respect to the semantics of definite descriptions. In honour of the pre-eminent figures who have inspired these positions, I will call them "the Meinongian view," "the Fregean view" and "the Russellian view." The last two views are the two mainstream views of definite descriptions, and they are each motivated in large part by their attempts to avoid untenable results typically associated with the Meinongian view. I propose, however, that there is a rendering of the Meinongian view of definite descriptions that is preferable to any renderings of the Fregean or Russellian views. The objective of my paper is limited to introducing this variant of the Meinongian view of definite descriptions and showing that it is preferable to any variant of the Fregean view. My conclusion is based on the observation that the Fregean view provides us with a truth-conditionally adequate analysis of a proposition expressed by a "simple sentence," such as sentence 1, but such an analysis cannot be extended to apply to propositions expressed by "non-simple sentences," such as those expressed by sentences 2 through 6. The New Meinongian Analysis, in contrast, provides a uniform analysis that is truth-conditionally adequate for all cases.
1. `The director of Schindler's List is injured.'
2. `The temperature in Calgary is rising.'
3. `The tallest building on earth was in Chicago.'
4. `The glacier in Kenya fails to exist.'
5. `The president of the United States might have been Gore.'
6. `The nuclear plant in New Zealand is being searched for by
DeNiro.
VISITING SPEAKER:
Claudio
Hermida
(Secção de Ciência da Computação,
Departamento de Matemática,
Instituto Superior Técnico, Lisboa, PORTUGAL)
Some Categorical Observations on Modal Logic and Simulation
Considering modalities for transition systems, we set up a basic categorical framework to interpret them. Starting with a category C with suitable structure, we give universal characterisations of the associated bicategories of spans, relations and partial maps. We then apply such characterisation to derive the first-order logic interpretation of modalities (reducing modal quantifiers to the usual existential/universal ones).
As a biproduct of the categorical interpretation of modalities, we present a novel view of the satisfaction of modal formulas as a simulation, thereby strenghtening the relationship between these concepts.
SPEAKER:
Richard Zach
(Department of Philosophy, University of Calgary)
Intuitionistic Fuzzy Logic and other Gödel Logics
In 1932, Kurt Gödel showed that propositional intuitionistic logic is not characterized by any finite matrix, i.e., that it is not the set of tautologies of any many-valued logic with finitely many truth values. In doing so, he introduced a family of logics, now called Gödel logics, which are intermediate in strength between classical and intuitionistic loigc. Dummett, in 1959, axiomatized the corresponding infinite valued logic (which coincides with the interesection of all finite-valued Gödel logics) as intuitionistic logic plus (A -> B) v (B -> A). This logic can be extended to a family of first-order logics, with truth values from closed subsets of the real interval [0, 1]. The logic based on the full interval [0, 1] has been investigated by Takeuti and Titani, and called Intuitionistic Fuzzy Logic. We present these logics and show that all but two are not axiomatizable. We give an axiomatization of intuitionistic fuzzy logic based on a hypersequent calculus. If time permits, we will also discuss related results about propositional entailment relations and compactness of propositional infinite-valued Gödel logics, and about propositional Gödel logics with quantifiers over truth values. (Joint work with Matthias Baaz)
VISITING SPEAKER:
Krzysztof Worytkiewicz
(Department of Computer Science, Swiss Federal Institute of Technology)
Generalized Simulations and Bimodular Modal Logic
ABSTRACT: We present a generalization of the triad lts's/ (bi)simulation/ Hennessy-Milner logic, appropriate to directly cope with issues peculiar to process exchanging values of arbitrary types and exhibiting imperative features. This generalization is analyzed and characterized abstractly by deploying relevant pieces of categorical machinery.
The processes under study are categorical transition systems, transposes under the free adjunction of graph homomorphisms from a `control graph' to a category of `elementary computations' in L. we propose the notion of dynamic simulation which essentially allows a transition to be matched by a possibly non-trivial control path provided the labels agree. Classic string simulation but also the classic weak one come about as special cases.
In our abstract treatment, bimodules i.e. morphisms of the bicategory B of free categories and discrete fibrational spans play the role of generalized relations. We characterize dynamic simulation over L in terms of the interaction between certain lax functors called `modules'. This boils down to a factorization through R: Cyl(B) -> BxB, the Grothendieck comprehension of the homomorphism B(-,-). On the logical side, we present the construction of a doctrine for a modal logic as a canonical extension of a regular fibration, here an account of the extension of a logic of `sets' and `functions' to a logic of `sets' and `bimodules'. We study its interaction with cts's and dynamic simulations and pin down the satisfaction relation over cts's as a universal dynamic simulation.
VISITING SPEAKER:
Christine Heitsch
(Department of Computer Science, University of British Columbia)
GENERALIZED PATTERN MATCHING and the Complexity of UNAVOIDABILITY TESTING
We formulate the GENERALIZED PATTERN MATCHING problem, a natural extension of string searching capturing regularities across scale. The special case of UNAVOIDABILITY TESTING is obtained by fixing an appropriate family of text strings -- the Zimin words. We investigate the complexity of this restricted decision problem. Although the efficiency of standard string searching is well-known, determining the occurrence of generalized patterns in Zimin words does not appear so tractable. Specifically, we provide an exponential lower bound on any algorithmic decision procedure relying exclusively on the equivalent deletion sequence characterization of unavoidable patterns. We also demonstrate that the four other known necessary conditions are not sufficient to decide pattern unavoidability.
SPEAKER:
Jeff Green
(Department of Computer Science, University of Calgary)
Partial Evaluation of Event Structures, Occurrence Nets, and Event Expressions.
Partial evaluation is a technique for optimizing a program within the context of specific input to the program. It contrasts with traditional optimizing techniques in that it is not part of the compilation process, or more specifically part of the compiler. The focus of this work is on exploring and producing partial evaluation techniques to apply to concurrent computation, specifically event structures. An algorithm for partially evaluating event structures is presented, and from there the foundation for establishing its correctness is built. This foundation is extended to incorporate a form of Petri nets, occurrence nets, that is equivalent to event structures and to a form of concurrent regular expressions called event expressions. The algorithm is extended to apply to occurrence nets and event expressions by composing it with invertible mappings from event structures to occurrence nets and event expressions. That composition provides a means to partially evaluate occurrence nets and event expressions.
VISITING SPEAKER:
R.A.G. Seely
(McGill University and John Abbott College)
Introduction to the Logic of Circuits
ABSTRACT: This talk will be a tutorial on the categorical proof theory of linear logic, with emphasis on the graphical techniques of the logic of circuits.
Luigi Santocanale
(Department of Computer Science, University of Calgary)
Parity Games: How to Play with Induction and Coinduction
ABSTRACT: I'll begin from automata theory: I'll recall theorems by Büchi and Rabin relating sets of (infinite) objects definable by means of Monadic Second Order Logic and sets of (infinite) objects recognized by automata. I'll point out that one can find automata in normal form: these are characterized by the parity acceptance condition. I'll explain the close relationship of these automata with parity games.
I'll show then how to associate to each parity game an algebraic expression, based on the categorical notions of products coproducts, initial algebras and final coalgebras (the last two are categorical formulations of induction and coinduction). I'll show that parity games can be considered as terms of a categorical theory, which turn out to be equivalent to categorical $\mu$-terms defining the property of a category of being $\mu$-bicomplete.
The category of sets and functions is $\mu$-bicomplete and when a parity game is algebraically interpreted in this category what we obtain is the set of deterministic winning strategies for a chosen player in this game.
Richard Zach
(Department of Philosophy, University of Calgary)
Intuitionistic Propositional Logic and S4 with Quantification over Propositions
In Kripke semantics for propositional intuitionistic and modal logic, a proposition can be identified with the set of worlds in which a propositional variable or a sentence is true. We accordingly obtain propositionally quantified intuitionistic or modal logics by adding quantifiers which range over subsets of the possible worlds. In general, this seemingly innocuous extension actually results in a significant increase in complexity of the resulting logics. For instance, Kremer has shown that both quantified propositional intuitionistic logic and S4 are recursively isomorphic to full-second order logic (and hence far from decidable), Antonelli established a similar result for bimodal S5. We show that quantified propositional logic and S4 remain decidable if the Kripke frames are restricted to trees.
Peter Zvengrowski
(Department of Mathematics, University of Calgary)
Categorical Properties of Compactly Generated Spaces I&II
ABSTRACT:
As the part of topology known as homotopy theory grew rapidly in the 1950s, the need for a "convenient" category of topological spaces which could be used to carry out the operations of homotopy theory (especially taking function spaces) became clear. In the period 1959-1964 several quite different solutions were proposed, notably by Milnor, Michael, and Spanier. However, a very influential paper by Steenrod in 1967 discusses the category of compactly generated Hausdorff spaces (which was by no means new) and shows that this category is indeed convenient (in a sense made precise by Steenrod). Since that time the textbooks on the subject have all adopted his approach and used this category.
In this talk, which will cover $n$ lectures ($1\leq n\leq 2$), the basic ideas of homotopy theory leading to these problems will first be discussed. Then the necessary topology to understand the compactly generated spaces will be developed, and some of the nice categorical properties such as regular, cartesian closed for this category. A couple of new results showing that certain very common function spaces of homotopy theory are indeed compactly generated will be given. A good exposition of all of this material and much more is in the M. Sc. thesis of my student A. Odunuga.
Dana Harrington
(Department of Computer Science, Calgary University)
Models of Uniqueness Logic
ABSTRACT: Uniqueness types capture the `single use' property for values. They enable many optimizations in programming languages, in particular unique types permit in-place updates of `unique' values. Uniqueness categories supply the proof theory for the logic of uniqueness types. We will review the definition of uniqueness categories and examine several models.
Luigi Santocanale
(Department of Computer Science, University of Calgary)
Fixed Point Logics and Circular Proofs
ABSTRACT: Fixed point logics and $\mu$-calculi are obtained from previously existing logical or algebraic frameworks by the addition of least and greatest fixed point operators. The propositional modal $\mu$-calculus or modal $\mu$-logic, useful for model checking, arises from modal logic exactly in this way.
A proposition-term in a $\mu$-calculus has a circular structure: it is possible to travel along subformulas and come back to the starting point using regenerations of fixed point. The circularity is inherited by proof-terms. Normally cut-free proofs in sequent calculi are finite because premiss sequents are always strictly smaller than conclusions. However, in settings where the propositions themselves can be circular, there exists the possibility of having circular or infinite proofs as well. Remarkably, in the theories of fixed points, these kind of proofs happen to be the most useful. Thus, the mathematics suggests that we are indeed allowed to make circular reasonings.
In this talk I'll explain this apparent paradox, using the concept of initial algebra of a functor. I'll point out the sense for which initial algebras of functors are a generalization of least fixed points and the relationship to inductively constructed sets (such as lists, finite tress, etc.).
I will interpret circular proofs as sort of functions (more precisely, arrows of a category) having as domain an inductively constructed set. Recall that recursively defined functions are uniquely determined by their defining system of equations. Similarly it is possible to transform a circular proof in a system of equations and then prove that this system admit a unique solution.
John Aldwinkle
(Department of Computer Science, University of Calgary)
Modal Logic for Model Checking
ABSTRACT:
King Henry the Fourth
Act III. Scene I.
Glendower I can call spirits from the vasty deep.
Hotspur Why, so can I, or so can any man;
But will they come when
you do call for them?
Glendower: I can write multi-threaded protocols.
Hotspur: Why, so can I, or so can any man;
But will
they work when you run them?
(apologies to Shakespeare)
Building concurrent systems, such as CPU's or other VLSI devices or writing computer communications protocols is fraught with peril; people are not good at recognising the implications of their designs.
Modal Logic is a language for reasoning about these systems, and Model Checkers perform this sort of reasoning automatically. For this reason, Model checking has become widely used by VLSI designers. The modal Mu logic underlies many of these model checkers.
This logic is the familiar modal logic K, augmented with fixed points.
I will give a tutorial level talk about the modal Mu logic and give some examples of how it can be used to check some VLSI devices.
John Aldwinckle
VISITING SPEAKER:
Richard J. Wood
(Department of Mathematics, Dalhousie University)
Tensor Products of Sup-lattices
ABSTRACT: We provide an alternate explicit description of the tensor product, M*N, of sup-lattices which facilitates discussion of sup-enriched categories and suggests generalization to total categories.
John Aldwinkle
(Department of Computer Science, Calgary University)
A Lightning Fast Introduction to Partial Orders, Lattices and Fixed Points
ABSTRACT: This talk is aimed at first year grad students. It consists
mainly of definitions and examples with a few simple theorems. Definitions
include, preorder, partial order, lattice, filter, ideal, equivalence relation/partition
(as examples of non distributive lattices), boolean lattices and chains.
It culminates with definitions of monotonic maps, prefixed point, post
fixed point, and least and greatest fixed point, and, finally, with Tarski's
fixed point theorem.
Some familiar examples of fixed points are presented, such at the transitive
closure of a set of relations (R*) and the "reachability" relation.
If there is time, I will have handouts.
Dana Harrington
(Department of Computer Science, Calgary University)
Uniqueness Logic and Uniqueness Categories
ABSTRACT: Uniqueness types are used in the Clean programming language to permit in-place modification of values without violating referential transparency. I will introduce `uniqueness logic', a logic whose formulae are equivalent to uniqueness types via a Curry-Howard `types as formulae' equivalence. Uniqueness logic is similar in spirit to linear logic in the sense of moderating the weakening and contraction rules via a modality. I will conclude with a discussion of `uniqueness categories', the categorical proof theory for uniqueness logic.
Xiuzhan Guo
(Department of Computer Science, Calgary University)
Descent Equivalences
ABSTRACT: Descent Theory was developed by Grothendick in Algebraic Geometry.
We shall give a brief introduction to Descent Theory, introduce the notion
of descent equivalence, and characterize absolute descent
equivalences.
Robin Cockett.
(Department of Computer Science, Calgary University)
The Free Restriction Category Generated by a Graph
ABSTRACT: A restriction category is a category X equipped with a combinator
f: A -> A |---> {f}:A -> A
satisfying the following four (independent )equations:
The free restriction category R(G) generated by a graph G has a particularly simple form:
(s,S):A -> B |----> ((A,[],A),S): A -> A
The category can be most clearly be presented by trees whose arcs are
labeled by the arrows in G and in which a node has been selected
to be the codomain.