Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain

This paper reports a case study in the use of proof planning in the context of higher order syntax. Rippling is a heuristic for guiding rewriting steps in induction that has been used successfully in proof planning inductive proofs using first order representations. Ordinal arithmetic provides a natural set of higher order examples on which transfinite induction may be attempted using rippling. Previously Boyer-Moore style automation could not be applied to such domains. We demonstrate that a higher-order extension of the rippling heuristic is sufficient to plan such proofs automatically. Accordingly, ordinal arithmetic has been implemented in lambda-clam, a higher order proof planning system for induction, and standard undergraduate text book problems have been successfully planned. We show the synthesis of a fixpoint for normal ordinal functions which demonstrates how our automation could be extended to produce more interesting results than the textbook examples tried so far.

Character, Audience Agency and Trans-Media Drama

Changes in the television industry with regards to the development of new media technologies are having a significant impact on audience engagement with television drama. This article explores how the internet is being used to extend audience engagement onto platforms other than the television set to the point where television drama should increasingly be reconsidered as trans-media drama. However audience engagement with the various elements of a trans-media drama text is complex. By exploring audience attitudes towards character in the British television series Spooks and its associated online games, this article argues that in an increasingly converged media landscape audiences transfer values between platforms. Consequently the audience's perception of control in relation to their engagement with a trans-media drama text such as Spooks becomes complicated with values associated with television proving key to their engagement with the same fictional world in the form of games.