11th Seminar on Algebra, Logic and Geometry in Informatics (ALGI):
Abstracts of Talks
[
Schedule and Participants (English)
|
Info
(Japanese)
|
ALGI Home
(Japanese,
English)
]
A Decidable Linear Logic for Speech Translation
The structure of objects employed in the study of Natural Language
Semantics has been increasingly being complicated to represent the
items of information conveyed by utterances. The complexity becomes
a source of troubles when we employ those theories in building
linguistic applications such as speech translation system. To
understand better how programs operating on semantic representations
work, we adopt a logical approach and present a monadic and
multiplicative linear logic. In designing the fragment, we refine on
the multiplicative conjunction to employ both the commutative and
non-commutative connectives. The commutative connective is used to
glue up a set of formulae representing a semantic object
conjointly. The non-commutative connective is used to glue up a list
of formulae representing the argument structure of an object, where
the order matters. We also introduce to our fragment a Lambek slash,
the directional implication, to concatenate the formula representing
the predicative part of the object and the list of formulae
representing the argument part. The monadic formulae encode each
element of the argument part by representing its sort with the
predicate and the element as the place-holder. The fragment enjoys
the nice property of being decidable. To encode contextual
information involved in utterances, however, we extend the fragment
with the exponential operator. The context is regarded as a resource
available as many as required, but not infinitely many. We encode
the items of context with the exponential operator, but ensure that
the operator should appear only in the antecedent. The extention
keeps the fragment decidable because the proof search will not fall
into an endless search caused by the coupling of unlimited supply
and consumption. We show that the fragment is rich enough to encode
and transform semantic objects employed in the contemporary
linguistic theories. The result guarantees that the theories on
natural language semantics can be implemented reasonably and safely
on computers.
Kleene Categories for Tree Languages
We define Kleene categories and a use of this notion to give an
account for regular tree languages. The case where the signature of
the trees are all unary specialises to the usual regular string
languages.
On Girard's New Denotational Semantics
The purpose of this talk is to discuss topics introduced by
J.Y-.Girard in the monograph titled ``Locus Solum''
(available from
Girard's page, manuscript, 2001).
The main notions dealt with will be ``locus'' and ``ludics''.
The ``locus'' stands for a new logic, obtained as an extention of
linear logic, called ``Locative Logic'' such that the duality still
holds and a new notion of location is added into the syntax.
The ``ludics'' is game semantics for Locative Logic which help
us understand the normalization interactively. Our discussion
includes an introduction to the theory and discussions on
related topics in other areas.
Beyond Regularity: Equational Tree Automata for
Associative and Commutative Theories
A new tree automata framework, named equational tree automata, is
presented. In the newly introduced setting, congruence closures of
recognized tree languages are recognizable. Furthermore, we prove the
union and intersection operations are closed in certain useful
cases. To compare with an early related work of Gilleron and Tison, we
discuss the relationship between a special Turing machine, called
linear bounded automata, and equational tree automata. As a result, we
reason about some decidability results. We further present the
hierarchy of 4 classes of tree languages.
Computational Effects and Enriched Lawvere Theories
In the late 1980's, Eugenio Moggi proposed using monads to give a
unified way to model computational effects such as state, exceptions,
nondeterminism and input/output. Here, we propose a different but, in
a precise sense, almost equivalent approach, using the concept of
Lawvere theory, suitably enriched. This keeps the mathematics closer
to the computational phenomena, supports a theory of modularity that
has hitherto been missing, and fits naturally with well structured
general development of structural operational semantics for at least
some such effects. Parts of the technical content of this work have
been done jointly with Martin Hyland, Gordon Plotkin, and others.
Primitive Recursive Analogues of Large Cardinals
For more than twenty years, several proof theorists have
investigated proof theoretic ordinals of set theoretic systems based
on KP (Kripke-Platek set theory). In order to obtain such ordinals,
they deal with several large cardinals and admissible ordinals. For
example, they first consider a certain large cardinal X and an
admissible ordinal A corresponding to X and a system KP* which is
based on KP and characterized by A, and next they define certain sets
of ordinals and functions by employing X (which are called ``Skolem
hulls and collapsing functions'') and, by using such sets and
functions, establish a primitive recursive structure which bears the
proof theoretic ordinal of KP*.
Observing their inventions such as Skolem hulls, collapsing
functions, and primitive recursive structures above, we can expect a
possibility of existence of primitive recursive ordinals corresponding
to large cardinals (and admissible ordinals) which are employed for
establishing the proof theoretic ordinals.
In this talk, we take two systems: KPi corresponding to the least
weakly inaccessible cardinal and KPM corresponding to the least weakly
Mahlo cardinal, and propose two primitive recursive ordinals to have
properties similar to those of the cardinals above. These ordinals are
obtained from primitive recursive structures established by Skolem
hulls and collapsing functions, which are defined by M.Rathjen
for establishing the proof theoretic ordinals of KPi and KPM.
On a Problem by Y. Akama and D. Takeuti
Tree Automata and Tree Constraints
We are interested in the question whether automata techniques can help to
solve constraints over trees.
Tree constraints are first-order formulas built over a given set of
predicate symbols with a fixed interpretation in a domain of trees. The
semantics of such a tree constraint is a relation over trees. Tree
automata, on the other hand, provide a mechanism to define sets of trees.
Tree automata are well-investigated; they are known to enjoy basically the
same nice properties than word automata.
Unfortunately, classical automata are not well equipped to recognize the
kind of relation that we can get as the semantics of a constraint. What is
missing is
-
a means to encode a (non-unary) relation, that is to recognize a language
of n-tuples of trees. The standard technique is to consider an alphabet
of n-tuples of symbols.
-
the ability of the automaton to perform tests, in particular equality and
diseqality tests. This is necessary since tree constraints may contain
explicit or implicit equations.
In the case of word automata both extensions pose no problem since they are
subsumed by the closure properties of word automata. The same holds for the
extension of tree automata to tuples, and it also holds at least in some
interesting special cases for the extension of tree automata by
tests. Unfortunately, we encounter severe problems if we want to combine
both extensions to tree automata.
We will discuss the (mostly negative) results that we have obtained for our
new class of tree automata, and we will illustrate the automata approach at
hand of the (still open) problem of entailment of non-structural subtype
constraints.
Domain Theoretic Account of Computability via Bottomed Sequences
Computability over a topological space is given via its embedding to
the set of infinite sequences in which $n$ bottomes are allowed to
exist. In this talk, we give the domain-theoretic account of
computation over $n$-bottom sequence space and its relation with
computation over topological spaces like $R$. As a result, we show
that a compact metric space $X$ is $n$-dimensional (n = 0,1,ldots,
infinite) if $X$ is homeomorphic to the set of minimum elements of the
limit space of an algebraic domain, whose limit space is
$n$-dimensional.