Transcript a certain answer to

An exercise in proving
undecidability
Balder ten Cate
Bertinoro 15/12/2006
Query answering under GAV
mappings
Input:
a GAV mapping m: ST
a source instance I
a target query 
Output: the “certain answers”

(I,J) |= m
J()
Complexity
• For conjunctive queries , the problem is in
LOGSPACE (by “unfolding”)
• For FO queries , it’s undecidable.
• This talk: There a fixed FO query  for which
computing the certain answers is undecidable.
(Corrolary: CERT(m, ) is not definable in FO/datalog/...)
More precisely
• Fact: There is a GAV mapping m: ST and a
Boolean FO query  over T such that the
following is undecidable:
Given a source instance I, is “Yes” a certain
answer to  ?
• Proof: by reduction from an undecidable
tiling problem.
Periodic tiling
• An undecidable problem:
Given a finite set of tile types
...
Can we tile any n  n square with these tiles
so that (a) neighboring tiles match, (b) the
first and last column coincide, and (c) the first
and last row coincide (n > 1) ?
Reduction to GAV answering
• Basic idea:
– The source instance I specifies the set of tile types
– The GAV mapping m (which is fixed) simply copies
all the information
– The FO query  (which is fixed) describes a
periodic tiling with the given tile types.
• “Yes” is a certain answer to  on source
instance I iff the set of tile types specified by I
admits no periodic tiling.
First attempt
• Source schema:
– A unary relation TT listing tile types
– Binary relations COMPH and COMPV specifying
horizontal and vertical compatibility
• The GAV mapping:
x (TTx  TT’x)
x (RHx  RH’ x)
x (RVx  RV’ x)
• Before we continue:
What is wrong with this attempt?
Bug fix
We need to make sure that ...
• no compatibilities are added in the target
Solution: represent incompatibilities
• no new tile types are added in the target
Solution: use extra relations so that “tampering
can be detected”
The correct reduction:
• Source schema:
– A unary relation TT listing tile types
– Binary relations INCOMPH and INCOMPV specifying
horizontal and vertical incompatibility
– Two binary relations coding a linear ordering of the
tile types and a corresponding successor relation.
• The GAV mapping copies everything (as before)
• The target query  describes a periodic tiling
using the given tile types (homework exercise,
for the solution see Börger- Grädel-Gurevich) .
Added in print
• Prof. Kolaitis found a simpler and more elegant proof
by reduction of the undecidable embedding problem
for finite semi-groups: “given a partial binary function,
can it be extended to a semi-group (over a possible
larger but finite carrier set)?”
–
–
–
–
Source schema: a single ternary relation R
Target schema: a single ternary relation R’
GAV mapping: xyz (Rxyz  R’xyz)
The target query  expresses that R’ is an associative total
function (this can be expressed in FO logic, even using only
-formulas).
• “Yes” is a certain answer to  on source instance I
iff the I(R) cannot be extended to a finite semi-group.