The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction

Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a bisimulation). We present an automation of coinductive theorem proving. This automation is based on the idea of proof planning. Proof planning constructs the higher level steps in a proof, using knowledge of the general structure of a family of proofs and exploiting this knowledge to control the proof search. Part of proof planning involves the use of failure information to modify the plan by the use of a proof critic which exploits the information gained from the failed proof attempt. Our approach to the problem was to develop a strategy that makes an initial simple guess at a bisimulation and then uses generalisation techniques, motivated by a critic, to refine this guess, so that a larger class of coinductive problems can be automatically verified. The implementation of this strategy has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell. We have developed a proof plan for coinduction and a critic associated with this proof plan. These have been implemented in CoClam, an extended version of Clam with encouraging results. The planner has been successfully tested on a number of theorems.

Release currents of IP₃ receptor channel clusters and concentration profiles

We simulate currents and concentration profiles generated by Ca2+ release from the endoplasmic reticulum (ER) to the cytosol through IP3 receptor channel clusters. Clusters are described as conducting pores in the lumenal membrane with a diameter from 6 nm to 36 nm. The endoplasmic reticulum is modeled as a disc with a radius of 1–12 mm and an inner height of 28 nm. We adapt the dependence of the currents on the trans Ca2+ concentration (intralumenal) measured in lipid bilayer experiments to the cellular geometry. Simulated currents are compared with signal mass measurements in Xenopus oocytes. We find that release currents depend linearly on the concentration of free Ca2+ in the lumen. The release current is approximately proportional to the square root of the number of open channels in a cluster. Cytosolic concentrations at the location of the cluster range from 25 μM to 170 μM. Concentration increase due to puffs in a distance of a few micrometers from the puff site is found to be in the nanomolar range. Release currents decay biexponentially with timescales of < 1 s and a few seconds. Concentration profiles decay with timescales of 0.125–0.250 s upon termination of release.

Reactive clusters on a membrane

We investigate the reaction dynamics of diffusive molecules with immobile binding partners. The fixed reactants build clusters that comprise just a few tens of molecules, which leads to small cluster sizes. These molecules participate in the reaction only if they are activated. The dynamics of activation is mapped to a time-dependent size of an active region within the cluster. We focus on the deterministic description of the dynamics of a single cluster. The spatial setup accounts for one of the most important determinants of the dynamics of a cluster, i.e. diffusional transport of reaction partners toward or away from the active region of the cluster. We provide numerical and analytical evidence that diffusion influences decisively the dynamic regimes of the reactions. The application of our methods to intracellular Ca²⁺ dynamics shows that large local concentrations saturate the Ca²⁺ feedback to the channel state control. That eliminates oscillations depending on this feedback.