Logicと形式言語 - formallang.memo

(メモ書き)

On Trees

• known: FO < FO(TC^1) < MSO=REGT=DSPACE(1)=NSPACE(1) < FO(DTC)=DSPACE(log n) ≦ FO(TC)=NSPACE(log n)
• open: MSO vs FO(TC^k) for k≧2
  • MSOの個々の論理式に応じてkを大きく取ればFO(TC^k)で書けるのでMSO≦FO(TC)だけど、固定のkではどうかは謎
  • MSOで書けないFO(TC^2)で書けるものがあるのは確か。
• FO(DTC)はtree上でもundecidable。

See

• Tiede & Kepser 2006
• Engelfriet & Hoogeboom 2007
• Cateand & Segoufin 2008
• and many many old texts...