The Anatomy of Innocence

We reveal a symmetric structure in the ho/n games model of innocent strategies, introducing rigid strategies, a concept dual to bracketed strategies. We prove a direct definability theorem of general innocent strategies with respect to a simply typed language of extended B¨ohm trees, which gives an operational meaning to rigidity in call-byname. A corresponding factorization of innocent strategies into rigid ones with some form of conditional as an oracle is constructed.

• Type: Conference
• Year: 2001
• Where: CSL
• Authors: Vincent Danos, Russell Harmer
• Keywords: Automated Reasoning, CSL 2001, General Innocent Strategies, Innocent Strategies, Rigid Strategies