Program invariants as fixedpoints

We argue that soundness and relative completeness theorems for Floyd-Hoare Axiom Systems ([3], [5], [18]) are really fixedpoint theorems. We give a characterization of program invariants as fixedpoints of functionals which may be obtained in a natural manner from the text of a program. We show that within the framework of this fixedpoint theory, soundness and relative completeness results have a particularly simple interpretation. Completeness of a Floyd-Hoare Axiom System is equivalent to the existence of a fixedpoint for an appropriate functional, and soundness follows from the maximality of this fixedpoint. The functionals associated with regular procedure declarations are similar to thepredicate transformers of Dijkstra; for nonregular recursions it is necessary to use a generalization of the predicate transformer concept which we call arelational transformer.     

Effectively given domains

A definition of the notion of an effectively given continuous cpo is provided. The importance of the notion lies in the fact that we can readily characterize the computable (partial) functions of arbitrary finite type over an effectively given domain. We show that the definition given here is closed under several important domain constructions, namely sum, product, function space, powerdomain and inverse limits (the last two in a restricted form); this permits recursive domain equations to be solved effectively.     

Recursive functions in a data base language for complex objects

The work presented in this paper demonstrates a new method for recursive queries in a complex object data base system. The method is called functional recursion. Most previous approaches express recursive queries by set oriented recursion, i.e. they allow us to define a set M recursively by an equation M = ƒ(M). In contrast to set oriented recursion, functional recursion as defined in this paper allows the user to define a function ƒ recursively by an equation ƒ = F(ƒ). As opposed to recursive functions written in a conventional programming language, the termination criterion which sometimes is rather complex does not have to be programmed by the user but is given implicitly. By providing appropriate parameters to a function, the user can integrate a selection into the recursion in a convenient and natural way. This is not the case for set oriented recursion. When using set recursion, the user is forced to formulate a query which computes more than really needed. It is the task of the optimizer then to push the subsequent selection into the recursion. This means that the user cannot write the query in a natural way and the system then has to figure out what the user wanted. All these problems are avoided when using recursive functions as defined in this paper. Moreover, a solution based on key oriented duplicate elimination is presented which solves the problem of lists and arithmetics in the context of recursive functions. The method is illustrated by bill-of-materials examples and by a railroad example.     

Multivariable system structure and parameter identification using the correlation method

This paper describes an algorithm for the structure determination and parameter identification of linear discrete-time multivariable systems from input-output measurements. The algorithm starts by determining the structure parameters of a certain canonical state space representation from an estimate of the correlation functions of the output sequence. Then the parameters of the A matrix are estimated from the estimated correlation functions using the recursive least squares method. Finally a normalized stochastic approximation algorithm is used for the estimation of the parameters of the B matrix from input-output measurements.     

Set theory for verification. II: Induction and recursion

A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs, and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski theorem over a suitable set.Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion.Recursive data structures are expressed by applying the Knaster-Tarski theorem to a set, such asV , that is closed under Cartesian product and disjoint sum.Worked examples include the transitive closure of a relation, lists, variable-branching trees, and mutually recursive trees and forests. The Schröder-Bernstein theorem and the soundness of propositional logic are proved in Isabelle sessions.     

Computation of recursive functionals using minimal initial segments

The following problem in the computation of partial recursive functionals is considered: Minimizing the length of initial segments of input functions containing all function values requested by a machine computing a partial recursive functional. A recursive functional F is constructed such that any algorithm for F has unbounded redundancy, i.e. it requests function values on inputs unboundedly larger than those on which the output of F depends. However, for any recursive functional F such that the length of the segment on which F depends is itself a recursive functional, a non-redundant machine for F can be effectively constructed. Also considered are machines on 0-1 sequences for which it is shown that a machine realizing a given level of significance in a universal test of randomness must have unbounded redundancy.     

Optimal linear recursive estimation with uncertain system parameters

In an estimation problem the statistics of various random processes involved may not be known exactly. Using linear state space modeling techniques, this lack of information can often be represented by allowing certain system model parameters to assume any of a finite set of possible known values with corresponding a priori known probabilities. In this short paper a recursive minimum variance estimator, restricted to be a linear function of the observation data sequence, is obtained for an estimation problem which can be described by a linear discrete time system model with uncertain parameters; all initial information relative to these uncertain parameters is utilized by the estimator. The estimation error covariance matrix, in a recursive form, is also obtained. An example is given to illustrate the usefulness of this estimator.     

Nondeterministic flowchart programs with recursive procedures: semantics and correctness I

In this paper, we study some aspects of the semantics of nondeterministic flowchart programs with recursive procedures. In the first part of this work we provide the operational semantics of programs using the concept of an execution tree. We propose a new definition of the semantics of a non-deterministic recursive program as a mapping from the input domain to the set of execution trees determined by the program. Using this new concept, we prove that every nondeterministic flowchart program with recursive procedures can be unfolded into a semantically equivalent infinite pure flowchart (without procedures). This result is applied in the second part of this work to prove the soundness of an inductive assertion method which is also complete with a finite number of assertions (contrary to De Bakker and Meertens's method [11]).     

A characterization of computable analysis on unbounded domains using differential equations

The functions of computable analysis are defined by enhancing normal Turing machines to deal with real number inputs. We consider characterizations of these functions using function algebras, known as real recursive functions. Since there are numerous incompatible models of computation over the reals, it is interesting to find that the two very different models we consider can be set up to yield exactly the same functions. Bournez and Hainry used a function algebra to characterize computable analysis, restricted to the twice continuously differentiable functions with compact domains. In our earlier paper, we found a different (and apparently more natural) function algebra that also yields computable analysis, with the same restriction. In this paper we improve earlier work, finding three function algebras characterizing computable analysis, removing the restriction to twice continuously differentiable functions and allowing unbounded domains. One of these function algebras is built upon the widely studied real primitive recursive functions. Furthermore, the proof of this paper uses our previously developed method of approximation, whose applicability is further evidenced by this paper.     

Partial Functions in ACL2

We describe a method for introducing “partial functions” into ACL2, that is, functions not defined everywhere. The function “definitions” are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions, and we discuss how such functions can be used to prove theorems about state machine models without reasoning about “clocks” or counting the number of steps until termination. Our macro for introducing “partial functions” also permits a variety of other recursive schemes, and we briefly illustrate some of them. This revised version was published online in August 2006 with corrections to the Cover Date.     

Some natural properties of strong-identification in inductive inference

In this paper the problem of inducing an algorithm for a partial recursive function from the analysis of its graph or loosely speaking of “learning” it, is discussed.A certain number of results are obtained mainly relatively to the question of whether, given a machine M able to learn all functions within a set C, one can construct a machine M' able to learn a new set C' related in some “natural” way to C, by using the experience of M.     

Consequence Verification of Flowcharts

A common basis is presented, for Floyd's method of inductive assertions and for the subgoal induction method of Morris and Wegbreit. This basis is provided by consequence verification, a method for verifying logic programs. We connect flowcharts with logic programs by giving a recursive definition of the set of all computations of a flowchart. This definition can be given in two ways: the recursion can run forward or backward. Both definitions can be expressed in logic, resulting in a logic program which is then subjected to consequence verification. Verification of the forward logic program is shown to be essentially Floyd's method; verification of the backward program corresponds similarly to subgoal induction.     

Verification of Systolic Array:An FP Functional Approach

There has been much interest in the use of formal techniques for the design and analysis ofsystolic arrays.One important aspect of analysis of systolic array is the correctness problem.A few attempts for the verification of systolic array have appeared in the literature.The deficiency is that all of these methods lack a straightforward way of proving correctness.They need either proposing a solution,then applying inductive techniques or showing that thearray satisfies three types of properties:safety,liveness and termination.In this paper,an FP functional approach is proposed.The goal is to verify that a givensystolie design computes the function for which it was intended,lnstead of the generation of asystolic architecture,the method generates a system of recursive functional equations whichdescribes the algorithm executed by the architecture.This representation consists of severalequations describing processes executed by local cells,equations describing connectionsbetween cells,functions representing data streams,and functions describing the relationbetween the structure of input and output data and the systolic array structures.The minimumsolution of the system of recursive functional equations is the function computed by the systolicarchitecture.The main advantage of this approach is that it allows us to develop an algebra offunctional programs. We have developed various methods to deal with different kinds ofsystems of functional recursive equations.By solving the system of recursive functionalequations,we can get the least solution directly.This provides a straightforward way forproving correctness.An example is given.A typical system of recursive functional equations is generated,which can represent most of systolic design.Algebra method is developed showing how to solvethis problem.     

基于目标函数的递推子空间辨识算法

针对实际工程中要求对系统参数进行在线估计的问题, 提出一种递推子空间辨识的新方法. 通过引入辅助变量关系将递推子空间辨识问题转化为目标函数的迭代最小化问题. 采用递推最小二乘算法在线估计参数并由传播方法得到更新的广义能观性矩阵, 进而求得子空间辨识模型系统参数. 该算法简单有效且对初值具有鲁棒性. 最后, 通过仿真实例验证算法的有效性.     

Motion planning for maintaining landmarks visibility with a differential drive robot

This work studies the interaction of non-holonomic and visibility constraints using a Differential Drive Robot (DDR) that has to keep static landmarks in sight in an environment with obstacles. The robot has a limited sensor, namely, it has a restricted field of view and bounded sensing range (e.g. a video camera). Here, we mean by visibility that a clear line of sight can be thrown between the landmark and the sensor mounted on the DDR. We first determine the necessary and sufficient conditions for the existence of a path such that our system is able to maintain one given landmark visibility in the presence of obstacles. This is done through a recursive, complete algorithm that uses motion primitives exhibiting local optimality, as they are locally shortest-lengths paths. Then, we extend this result to the problem of planning paths guaranteeing visibility among a set of landmarks, e.g. to observe a given sequence of landmarks or to observe at each point of the path at least one element of the landmarks set. We also provide a procedure that computes the robot controls yielding such a path.¹     

ITERATIVE AND RECURSIVE ALGORITHMS FOR TREE SEARCH AND PARTITION SEARCH OF THE LATTICE OF STRUCTURE MODELS

An important problem in reconstructability analysis, and modelling in general, is determination of the set of simplest models, all of which acceptably represent the information contained in a given overall system. Evaluation of these models depends on acceptability (semantic) criteria and structural criteria. Structural criteria determine whether one model is simpler than another. In this paper we assume the existence of acceptability criteria and mechanisms to determine if given models meet them. The general problem we solve is how to most efficiently generate the set of all models. We use these results to determine the set of simplest models that satisfy the acceptability criteria

The main results of the paper are: a procedural definition of a recursive Boolean lattice that is based on recursive partitioning of the set of models, a definition of a spanning tree of the lattice of models, and algorithms for non-duplicating generation and search of the lattice of models. The generation and search algorithms fall into two categories: (i) iterative and recursive algorithms that implement the definition of the spanning tree and use it to determine the set of simplest models; (ii) algorithms that implement recursive partition search of the lattice of models. Two algorithms for recursive partition search are given, one that applies the procedural definition of a recursive Boolean lattice to the full set of models, and one that first partitions the full set into C-Structure equivalence classes, and then applies the definition of the recursive Boolean lattice to the equivalence classes.     

Preference functions for prediction of membrane-buried helices in integral membrane proteins

The preference functions method is described for prediction of membrane-buried helices in membrane proteins. Preference for the α-helix conformation of amino acid residue in a sequence is a non-linear function of average hydrophobicity of its sequence neighbors. Kyte–Doolittle hydropathy values are used to extract preference functions from a training data set of integral membrane proteins of partially known secondary structure. Preference functions for β-sheet, turn and undefined conformation are also extracted by including β-class soluble proteins of known structure in the training data set. Conformational preferences are compared in tested sequence for each residue and predicted secondary structure is associated with the highest preference. This procedure is incorporated in an algorithm that performs accurate prediction of transmembrane helical segments. Correct sequence location and secondary structure of transmembrane segments is predicted for 20 of 21 reference membrane polypeptides with known crystal structure that were not included in the training data set. Comparison with hydrophobicity plots revealed that our preference profiles are more accurate and exhibit higher resolution and less noise. Shorter unstable or movable membrane-buried α-helices are also predicted to exist in different membrane proteins with transport function. For instance, in the sequence of voltage-gated ion channels and glutamate receptors, N-terminal parts of known P-segments can be located as characteristic α-helix preference peaks. Our e-mail server: predict@drava.etfos.hr, returns a preference profile and secondary structure prediction for a suspected or known membrane protein when its sequence is submitted.     

Including shape handles in recursive subdivision surfaces

In the present paper, the problem of the generation of an interpolating surface for a given, general polyhedron is studied. The surface must interpolate the set of vertices of the initial polyhedron, and allow a certain shape control. A two-step process based on a topological modification of the polyhedron, and a subsequent biquadratic recursive subdivision is used. It allows the definition of a set of scalar shape handles associated to the initial vertices, that do not affect the interpolatory properties of the surface. Their effect on the quality of the final shape is discussed, and an iterative algorithm for the computation of an optimal set of shape handles is proposed.