Habilitationsschrift--München, 1977. / Bibliography: p. 105-107.

No description available.

Thesis (M.S. in Applied Mathematics)--Naval Postgraduate School, June 2002. / Thesis advisor(s): Harold Fredricksen, Craig W. Rasmussen. Includes bibliographical references (p. 45-46). Also available online.

This work is an exploration into the palindrome, both as a literary form and an expression of infinity. The first two chapters address the fascinating manner in which the mind contextualizes fragments of speech and ludicrous grammatical implications that are spawned by the poetic structure of the palindrome (third chapter). The thesis then departs from the literary aspect of the palindrome and focuses in the fourth chapter on structural likenesses in psychology and mythology. The fifth chapter argues the palindrome and parallel conceptual structures as examples of recursion, then presents examples of recursion in language/grammar, art, and computer science. The sixth chapter uses instances of the recursive equiangular spiral throughout nature to introduce recursion and therefore the palindrome as an archetypal expression of infinity. The thesis ends with a list of the author's palindromes.

Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 1980. / Vita. / Bibliography: leaves 161-163. / by Edward R. Griffor. / Thesis (Ph.D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 1980.

No description available.

No description available.

Inductive definitions are the most natural means by which to represent many families of structures occurring in mathematics and computer science, and their corresponding induction / recursion principles provide the fundamental proof techniques by which to reason about such families. This thesis studies formal proof systems for inductive definitions, as needed, e.g., for inductive proof support in automated theorem proving tools. The systems are formulated as sequent calculi for classical first-order logic extended with a framework for (mutual) inductive definitions. The default approach to reasoning with inductive definitions is to formulate the induction principles of the inductively defined relations as suitable inference rules or axioms, which are incorporated into the reasoning framework of choice. Our first system LKID adopts this direct approach to inductive proof, with the induction rules formulated as rules for introducing atomic formulas involving inductively defined predicates on the left of sequents. We show this system to be sound and cut-free complete with respect to a natural class of Henkin models. As a corollary, we obtain cut-admissibility for LKID. The well-known method of infinite descent `a la Fermat, which exploits the fact that there are no infinite descending chains of elements of well-ordered sets, provides an alternative approach to reasoning with inductively defined relations. Our second proof system LKIDw formalises this approach. In this system, the left-introduction rules for formulas involving inductively defined predicates are not induction rules but simple case distinction rules, and an infinitary, global soundness condition on proof trees — formulated in terms of “traces” on infinite paths in the tree — is required to ensure soundness. This condition essentially ensures that, for every infinite branch in the proof, there is an inductive definition that is unfolded infinitely often along the branch. By an infinite descent argument based upon the well-foundedness of inductive definitions, the infinite branches of the proof can thus be disregarded, whence the remaining portion of proof is well-founded and hence sound. We show this system to be cutfree complete with respect to standard models, and again infer the admissibility of cut. The infinitary system LKIDw is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e. to those proofs representable by finite graphs. This restricted “cyclic” proof system, CLKIDw, is suitable for formal reasoning since proofs have finite representations and the soundness condition on proofs is thus decidable. We show how the formulation of our systems LKIDw and CLKIDw can be generalised to obtain soundness conditions for a general class of infinite proof systems and their corresponding cyclic restrictions. We provide machinery for manipulating and analysing the structure of proofs in these essentially arbitrary cyclic systems, based primarily on viewing them as generating regular infinite trees, and we show that any proof can be converted into an equivalent proof with a restricted cycle structure. For proofs in this “cycle normal form”, a finitary, localised soundness condition exists that is strictly stronger than the general, infinitary soundness condition, but provides more explicit information about the proof. Finally, returning to the specific setting of our systems for inductive definitions, we show that any LKID proof can be transformed into a CLKIDw proof (that, in fact, satisfies the finitary soundness condition). We conjecture that the two systems are in fact equivalent, i.e. that proof by induction is equivalent to regular proof by infinite descent.

Reconfigurable computing is a method of development that provides a developer with the ability to reprogram a hardware device. In the specific case of FPGAs this allows for rapid and cost effective implementation of hardware devices when compared to standard a ASIC design, coupled with an increase in performance when compared to software based solutions. With the advent of development tools such as Celoxica's DK package and Xilinx's Forge package, that support languages traditionally associated with software development, a change in the skill sets required to develop FPGA solutions from hardware designers to software programmers is possible and perhaps desirable to increase the adoption of FPGA technologies. To support developers with these skill sets tools should closely mirror current software development tools in terms of language, syntax and methodology, while at the same time both transparently and automatically take advantage of as much of the increased performance that reconfigurable architectures can provide over traditional software architectures by utilizing the parallelism and the ability to create arbitrary depth pipelines which is not present in traditional microprocessor designs. A common feature of many programming languages that is not supported by many higher level design tools is recursion. Recursion is a powerful method used to elegantly describe many algorithms. Recursion is typically implemented by using a stack to store arguments, context and a return address for function calls. This however limits the controlling hardware to running only a single function at any moment which eliminates an algorithm's ability to take advantage of the parallelism available between successive iterations of a recursive function. This squanders the high amount of parallelism provided by the resources on the FPGA thus reducing the performance of the recursive algorithm. This thesis presents a method to address the lack of support for recursion in design tools that exploits the parallelism available between recursive calls. It does this by unrolling the recursion into a pipeline, in a similar manner to the pipeline obtained from loop unrolling, and then streaming the data through the resulting pipeline. However essential differences between loops and recursive functions such as multiple recursive calls in a function, and hence multiple unrollings, and post-recursive statements add further complexity to the issue of unrolling as the pipeline may take a non-linear shape and contain heterogeneous stages. Unrolling the recursive function on the FPGA increases the parallelism available, however the depth of the pipline and therefore the amount of parallelism available, is limited by the finite resources on the FPGA. To make efficient use of the resources on the FPGA the system must be able to unroll the function in a way to best suit the input but also must ensure that the function is not unrolled past its maximum recursive depth. A trivial solution such as unrolling on-demand introduces a latency into the system when a further instance of the function is unrolled that reduces overall performance. To reduce this penalty it is desirable for the system to be able to predict the behaviour of the recursive function based on the input data and unroll the function to a suitable length prior to it being required. Accurate prediction is possible in cases where the condition for recursion is a simple function on the arguments, however in cases where the condition for recursion is based on complex functions, such as the entire recursive function, accurate prediction is not possible. In situations such as this a heuristic is used which provides a close approximation to the correct depth of recursion at any given time. This prediction allows the system to reduce the performance penalty from real time unrolling without over utilization of the the FPGA resources. Results obtained demonstrate the increase in performance for various recursive functions obtained from the increased parallelism, when compared to a stack based implementation on the same device. In certain instances due to constraints on hardware availability results were gained from device simulation using a simulator developed for this purpose. Details of this simulator are presented in this thesis.

Thesis (Ph. D.)--University of Chicago, Dept. of Mathematics, June 2003. / Includes bibliographical references. Also available on the Internet.