[logic-ml] Talk by Prof. Sebastian Maneth

[Keisuke Nakano]

皆様，
(複数のメーリングリストに送信しています．重複して受信された場合はご容赦願います)

電気通信大学の中野と申します．

来る5月26日(金)，ブレーメン大学のSebastian Maneth先生がご講演を行います．
木トランスデューサ理論とその応用についてお話ししていただきますので，
お時間のある方は是非ご参加ください．

日時： 2017年5月26日(金) 15:00-17:00
場所： 電気通信大学西9号館3階AVホール
       http://www.uec.ac.jp/about/profile/access/pdf/map.pdf
　　　 (こちらの地図の68番の建物です．地図にはありませんが68番の南側に
　　　　門が設置されましたので，そちらをご利用されると便利です)

講演者：Prof. Sebastian Maneth (University of Bremen)

タイトル：View-Query Determinacy for Tree Transducers

概要：
This talk consists of two parts each with a duration of approximately 40 minutes.

The first part focuses on the view-query determinacy problem. 
Given transformations v and q, the problem asks whether there 
exists a function f such that f(v(s))=q(s) for all possible inputs s. 
View-query determinacy is a strong static analysis with many 
important applications; for instance, it was used by Buneman, 
Davidson and Frey for data citation [CACM 59 (2016)].
For tree transducers, Hashimoto, Sawada, Ishihara, Seki, and
Fujiwara showed in 2013 that determinacy is decidable for views realized by
extended linear bottom-up tree transducers, and queries realized by 
single-valued bottom-up tree transducers. Their solution tests 
functionality of the inverse of the view composed with the query.
We extend this result using known results about transducers and properties 
of uniformizers. A uniformizer of a relation R is a function 
that has the same domain as R. A query q is determined by a  view v 
if and only if the composition v ; u ; q is equivalent to q, where u is
a uniformizer of the inverse of v. Thus, our technique reduces the determinacy
problem to the existence of uniformizers and to the decidability of equivalence.
Henceforth, recent new results on decidability of equivalence immediately give
rise to new results about determinacy.

These results about transducer determinacy only work for views given by
linear (extended) transducers. It is easy to see that even if a view transducer copies 
once, at the input root node, then determinacy becomes undecidable. 
This is unfortunate, because some very basic translations cannot be realized by linear
transducers but require copying. Consider for instance a view that regroups 
a list of publications into sublists of books, articles, etc. A tree transducer realizing 
this view needs copying (i.e., it needs to process the original list multiple times).
The issue that we cannot deal with non-linear views lead us to study transducers 
with origin (Part 2 of the talk). Under origin semantics, transducers that produce their
output in "different ways" are considered different, even if they realize the same tree
translation. Under this more rigid semantics, determinacy can be decided even for 
non-linear views. In particular, origin determinacy is decidable if the view and query are 
either both given by deterministic top-down tree transducers with look-ahead, or, if 
they are both given by deterministic MSO definable transducers. Intuitively, the world 
becomes safer with origin, but more restrictive (e.g., the query “is book X before 
article Y in the original list?” becomes determined under origin semantics).

--
中野 圭介 <ksk at cs.uec.ac.jp>
電気通信大学 大学院情報理工学研究科
http://millsmess.cs.uec.ac.jp/~ksk/