Recursive Comprehension

2019 ◽  
pp. 130-153
Author(s):  
John Stillwell
Keyword(s):  
Fixed Point ◽  
Jordan Curve ◽  
Axiom System ◽  
Extreme Value ◽  
Uniform Continuity ◽  
Computable Analysis ◽  
Different Levels

This chapter proves the equivalences between the weak König lemma and the Heine–Borel, extreme value, and uniform continuity theorems. It also discusses the equivalence of the weak König lemma with two famous theorems of topology: the Brouwer fixed point and the Jordan curve theorems. This latter collection of theorems, lying strictly between RCA0 and ACA0, establishes the importance of the system WKL0 whose set existence axiom is the weak König lemma. Between them, RCA0, WKL0, and ACA0 cover the basic theorems of analysis, and they sort them into three different levels of strength. Here, RCA0 can be viewed as an axiom system for “computable analysis.” Its set existence axiom, called recursive comprehension, states the existence of computable sets.

scholarly journals A Proof of Constructive Version of Brouwer's Fixed Point Theorem with Uniform Sequential Continuity

2011 ◽  
Vol 2011 ◽  
pp. 1-9
Author(s):  
Yasuhito Tanaka
Keyword(s):  
Fixed Point ◽  
Fixed Point Theorem ◽  
Point Theorem ◽  
Uniform Continuity ◽  
Constructive Mathematics ◽  
Sperner’S Lemma ◽  
Brouwer’S Fixed Point Theorem ◽  
Constructive Version ◽  
Sequential Continuity ◽  
Brouwer's Fixed Point Theorem

It is often said that Brouwer's fixed point theorem cannot be constructively proved. On the other hand, Sperner's lemma, which is used to prove Brouwer's theorem, can be constructively proved. Some authors have presented a constructive (or an approximate) version of Brouwer's fixed point theorem using Sperner's lemma. They, however, assume uniform continuity of functions. We consider uniform sequential continuity of functions. In classical mathematics, uniform continuity and uniform sequential continuity are equivalent. In constructive mathematics a la Bishop, however, uniform sequential continuity is weaker than uniform continuity. We will prove a constructive version of Brouwer's fixed point theorem in an n-dimensional simplex for uniformly sequentially continuous functions. We follow the Bishop style constructive mathematics.

A PDL APPROACH FOR QUALITATIVE VELOCITY

2011 ◽  
Vol 19 (01) ◽  
pp. 11-26 ◽  
Author(s):  
A. BURRIEZA ◽  
E. MUÑOZ-VELASCO ◽  
M. OJEDA-ACIEGO
Keyword(s):  
Programming Languages ◽  
Moving Objects ◽  
Spatial Reasoning ◽  
Axiom System ◽  
Qualitative Reasoning ◽  
The Other ◽  
Other Hand ◽  
Order Of Magnitude ◽  
The One ◽  
Different Levels

We introduce the syntax, semantics, and an axiom system for a PDL-based extension of the logic for order of magnitude qualitative reasoning, developed in order to deal with the concept of qualitative velocity, which together with qualitative distance and orientation, are important notions in order to represent spatial reasoning for moving objects, such as robots. The main advantages of using a PDL-based approach are, on the one hand, all the well-known advantages of using logic in AI, and, on the other hand, the possibility of constructing complex relations from simpler ones, the flexibility for using different levels of granularity, its possible extension by adding other spatial components, and the use of a language close to programming languages.

scholarly journals Bounds for the Availabilities of Multistate Monotone Systems Based on Decomposition into Stochastically Independent Modules

2012 ◽  
Vol 44 (1) ◽  
pp. 292-308
Author(s):  
J. Gåsemyr
Keyword(s):  
Fixed Point ◽  
Complex Systems ◽  
Upper Bounds ◽  
Reliability Theory ◽  
Lower And Upper Bounds ◽  
Minimal Path ◽  
Monotone Systems ◽  
Modular Decomposition ◽  
The Relationship ◽  
Different Levels

Multistate monotone systems are used to describe technological or biological systems when the system itself and its components can perform at different operationally meaningful levels. This generalizes the binary monotone systems used in standard reliability theory. In this paper we consider the availabilities and unavailabilities of the system in an interval, i.e. the probabilities that the system performs above or below the different levels throughout the whole interval. In complex systems it is often impossible to calculate these availabilities and unavailabilities exactly, but it is possible to construct lower and upper bounds based on the minimal path and cut vectors to the different levels. In this paper we consider systems which allow a modular decomposition. We analyse in depth the relationship between the minimal path and cut vectors for the system, the modules, and the organizing structure. We analyse the extent to which the availability bounds are improved by taking advantage of the modular decomposition. This problem was also treated in Butler (1982) and Funnemark and Natvig (1985), but the treatment was based on an inadequate analysis of the relationship between the different minimal path and cut vectors involved, and as a result was somewhat inaccurate. We also extend to interval bounds that have previously only been given for availabilities at a fixed point of time.

Research on Driver Design for CMOS Image Sensor Based on DM642

2013 ◽  
Vol 321-324 ◽  
pp. 994-997
Author(s):  
Ping Xian Yang ◽  
Zhen Bao Liu ◽  
Tao Jin
Keyword(s):  
Fixed Point ◽  
Digital Signal Processor ◽  
Digital Signal ◽  
Image Sensor ◽  
Image Sensors ◽  
Video Capture ◽  
Sensor Interface ◽  
Cmos Image Sensors ◽  
Cmos Sensor ◽  
Different Levels

This paper mainly researches on the TI company fixed-point digital signal processor TMS320DM642 video capture technology for CMOS image sensors, sensor interface and video mini-driver carried out a detailed analysis, established different levels of peripheral structures under different CMOS Sensor, the research in this field has flexible characteristics and high practical value.

Continuous Families of Curves

1966 ◽  
Vol 18 ◽  
pp. 529-537 ◽  
Author(s):  
Branko Grünbaum
Keyword(s):  
Fixed Point ◽  
Jordan Curve ◽  
Convex Sets ◽  
General Setting ◽  
Jordan Curve Theorem ◽  
Planar Line ◽  
Families Of Curves ◽  
Planar Convex ◽  
Free Involution

The present paper is an attempt to find the unifying principle of results obtained by different authors and dealing—in the original papers—with areabisectors, chords, or diameters of planar convex sets, with outwardly simple planar line families, and with chords determined by a fixed-point free involution on a circle. The proofs in the general setting seem to be simpler and are certainly more perspicuous than many of the original ones. The tools required do not transcend simple continuity arguments and the Jordan curve theorem. The author is indebted to the referee for several helpful remarks.

scholarly journals Bounds for the Availabilities of Multistate Monotone Systems Based on Decomposition into Stochastically Independent Modules

2012 ◽  
Vol 44 (01) ◽  
pp. 292-308 ◽  
Author(s):  
J. Gåsemyr
Keyword(s):  
Fixed Point ◽  
Complex Systems ◽  
Upper Bounds ◽  
Reliability Theory ◽  
Lower And Upper Bounds ◽  
Minimal Path ◽  
Monotone Systems ◽  
Modular Decomposition ◽  
The Relationship ◽  
Different Levels

Multistate monotone systems are used to describe technological or biological systems when the system itself and its components can perform at different operationally meaningful levels. This generalizes the binary monotone systems used in standard reliability theory. In this paper we consider the availabilities and unavailabilities of the system in an interval, i.e. the probabilities that the system performs above or below the different levels throughout the whole interval. In complex systems it is often impossible to calculate these availabilities and unavailabilities exactly, but it is possible to construct lower and upper bounds based on the minimal path and cut vectors to the different levels. In this paper we consider systems which allow a modular decomposition. We analyse in depth the relationship between the minimal path and cut vectors for the system, the modules, and the organizing structure. We analyse the extent to which the availability bounds are improved by taking advantage of the modular decomposition. This problem was also treated in Butler (1982) and Funnemark and Natvig (1985), but the treatment was based on an inadequate analysis of the relationship between the different minimal path and cut vectors involved, and as a result was somewhat inaccurate. We also extend to interval bounds that have previously only been given for availabilities at a fixed point of time.

Sign in / Sign up

Export Citation Format

Share Document