A lambda calculus for real analysis
A lambda calculus for real analysis
复制标题
用于实分析的 lambda 演算
DOI：
10.4115/jla.2010.2.5
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
P. Taylor
中科院分区：
文献类型：
--
作者：
P. Taylor
摘要 Stone 对偶性是一般拓扑的一种新范式，其中可计算的连续函数被直接描述，而不使用集合论、无限格论或离散计算的先验理论。微积分中的每个表达式都表示一个连续函数和一个程序，其推理看起来非常像经典拓扑中的净化形式。这是针对普通数学家的 ASD 简介，以及在初等实分析中的应用。该语言应用于中值定理：实线上连续函数方程的解。众所周知，从数值和构造性考虑来看，如果函数“徘徊”在 0 附近，则方程无法求解，而永远找不到切向解。在 ASD 中，这两种失败以及在方程存在时寻找解的一般方法都可以通过新的显性概念来解释。零不是作为集合而是由更高类型的模态运算符捕获的。与映射的布劳威尔度不同，这些度是自然定义的，并且（斯科特）在参数方程的奇点上连续。用连续函数而不是使用点集来表达拓扑导致对非常接近格（或德摩根）对偶的开放和封闭概念的处理，而没有直觉方法中发现的双重否定。在此，紧凑性的双重性就是公开性。尽管区域理论中的相遇和连接是不对称的有限和无限，但它们在 ASD 中具有明显和紧凑的索引。公开性取代了度量属性（例如总有界性）和基数条件（例如具有可数稠密子集）。它还与构造分析中的定位性和递归理论中的递归可枚举性有关。
Abstract Stone Duality is a new paradigm for general topology in which computable continuous functions are described directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis. This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function "hovers" near 0, whilst tangential solutions will never be found. In ASD, both of these failures, and the general method of finding solutions of the equation when they exist, are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree of a mapping, these are naturally defined and (Scott) continuous across singularities of a parametric equation. Expressing topology in terms of continuous functions rather than using sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD. Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.