The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs

This paper reports the use of proof planning to diagnose errors in program code. In particular it looks at the errors that arise in the base cases of recursive programs produced by undergraduates. It describes two classes of error that arise in this situation. The use of test cases would catch these errors but would fail to distinguish between them. The system adapts proof critics, commonly used to patch faulty proofs, to diagnose such errors and distinguish between the two classes. It has been implemented in Lambda-clam, a proof planning system, and applied successfully to a small set of examples.

Exotic dynamics in a firing rate model of neural tissue with threshold accommodation

Many of the equations describing the dynamics of neural systems are written in terms of firing rate functions, which themselves are often taken to be threshold functions of synaptic activity. Dating back to work by Hill in 1936 it has been recognized that more realistic models of neural tissue can be obtained with the introduction of state-dependent dynamic thresholds. In this paper we treat a specific phenomenological model of threshold accommodation that mimics many of the properties originally described by Hill. Importantly we explore the consequences of this dynamic threshold at the tissue level, by modifying a standard neural field model of Wilson-Cowan type. As in the case without threshold accommodation classical Mexican-Hat connectivity is shown to allow for the existence of spatially localized states (bumps) in both one and two dimensions. Importantly an analysis of bump stability in one dimension, using recent Evans function techniques, shows that bumps may undergo instabilities leading to the emergence of both breathers and traveling waves. Moreover, a similar analysis for traveling pulses leads to the conditions necessary to observe a stable traveling breather. In the regime where a bump solution does not exist direct numerical simulations show the possibility of self-replicating bumps via a form of bump splitting. Simulations in two space dimensions show analogous localized and traveling solutions to those seen in one dimension. Indeed dynamical behavior in this neural model appears reminiscent of that seen in other dissipative systems that support localized structures, and in particular those of coupled cubic complex Ginzburg-Landau equations. Further numerical explorations illustrate that the traveling pulses in this model exhibit particle like properties, similar to those of dispersive solitons observed in some three component reaction-diffusion systems. A preliminary account of this work first appeared in S Coombes and M R Owen, Bumps, breathers, and waves in a neural network with spike frequency adaptation, Physical Review Letters 94 (2005), 148102(1-4).