|発表者の紹介||University of Oxford|
|タイトル||A Game-Semantic Model of Higher-Order Computation|
On the one hand, game semantics has been a highly successful approach
to (mathematical or denotational) semantics of logic and computation; it
gives a syntax-independent characterization of various logical systems
and programming languages in an intuitively natural, mathematically
precise and unified manner. However, it cannot capture step-by-step
computational processes, which in particular prohibits it from being a
mathematical model of computation in the sense of Turing machines,
though it has a good potential to overcome this point.
On the other hand, there are various mathematical models of
higher-order computation; however, they are mostly syntactic, axiomatic
(and inductive) or extrinsic (i.e., reducing higher-order computability
to the standard Church-Turing computability by coding). This situation
is unsatisfactory, particularly for Turing machines give a semantic,
non-axiomatic and intrinsic foundation of classical computation (i.e.,
computation on natural numbers).
Motivated by these points, I have extended game semantics into a
mathematical model of computation that defines higher-order
computability in a semantic, non-axiomatic and intrinsic manner, and
proved as a main theorem that it is Turing complete when restricted to
classical computation. As immediate corollaries, some of the well-known
theorems in computability theory such as the smn-theorem and the first
recursion theorem are generalized.
In the first half of the talk, I explain the background and the
motivation, and then give a brief introduction to game semantics. Then
in the second half, I talk about my work on higher-order computability
and more generally on theory of computation, where I focus on main ideas
and points rather than technical details. Finally, I draw a conclusion
and propose some future work.