12/15(月)のJohn Powerの余帰納的論理プログラミングの話、面白そう。 http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar

John Power (U. Bath), Coalgebraic Logic Programming: from Semantics to Implementation; embracing the laxness (joint with Ekaterina Komendantskaya)
Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops.  Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. However, the programming developments have often occurred separately and have usually been implementation-led.

Here, we start to give a coherent semantics-led account of the issues, proceeding from abstract category theoretic semantics and developing coalgebra to try to characterise naturally arising trees. As part of the project but not presented in this talk, the work is proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.