Seminars in August 2008

  • Heesung Shin (신희성), Counting labelled trees with given indegree sequence
    Counting labelled trees with given indegree sequence
    Heesung Shin (신희성)
    Institut Camille Jordan, Université Claude Bernard Lyon 1, France.
    2008/08/21 Thu, 4PM-5PM

    For a labeled tree on the vertex set [n]:={1,2,…,n}, define the direction of each edge ij as i to j if i<j. The indegree sequence λ=1e12e2 … is then a partition of n-1. Let aλ be the number of trees on [n] with indegree sequence λ. In a recent paper (arXiv:0706.2049v2) Cotterill stumbled across the following remarkable formulas a_\lambda = \dfrac{(n-1)!^2}{(n-k)! e_1! (1!)^{e_1} e_2! (2!)^{e_2} \ldots} where k = Σi ei. In this talk, we first construct a bijection from (unrooted) trees to rooted trees which preserves the indegree sequence. As a consequence, we obtain a bijective proof of the formula. This is a joint work with Jiang Zeng.</div>

    Tags:

  • Chung-Kil Hur (허충길), Term Equational Systems and Logics
    Term Equational Systems and Logics
    Chung-Kil Hur (허충길)
    Computer Laboratory, University of Cambridge, Cambridge, UK.
    2008/08/11 Mon, 4PM-5PM

    Equational reasoning is fundamental in automated theorem proving (that is, the proving of mathematical theorems by a computer program), and rewriting is a powerful method for equational reasoning. Category theory is a mathematical theory that deals in an abstract way with mathematical structures and relationships between them.

    Using category theory, we have developed a framework for equational reasoning. A Term Equational System (TES) is given by a semantic universe and an abstract notion of syntax; and given this, we automatically derive a sound logical deduction system, called Term Equational Logic (TEL). Furthermore, we provide an algebraic free construction for the system, which may be used to synthesize a sound and complete rewriting system for it.

    Existing systems arising in this framework include:

    • first-order equational logic and rewriting system;
    • combinatory reduction system of Klop;
    • binding equational logic and rewriting system of Hamana; and
    • nominal equational logics independently developed by Gabbay and Matheijssen, and Clouston and Pitts.

     

    Especially, following the above scenario in our framework, we have newly developed a sound and complete rewriting system for nominal equational logic.

    In this talk, rather than going into the technical details, I will focus on explaining basic ideas of category theory and how it can be used in practice.

    This is joint work with Marcelo Fiore.

    Tags:

Monthly Archives