Estoy tratando de envolver mi cabeza alrededor de la noción de apartness constructiva en matemáticas y resulta que me falta comprensión miserablemente.
Me gustaría usar como nociones elementales de lo posible, en el mejor de los casos en forma de $\lambda$-términos o algoritmos en enteros.
Recordemos algunas definiciones:
- Un número real $x$ es una tupla consistente en un mapa de $x: \mathbb{N} \longrightarrow \mathbb{Q} $ (poco abuso de notación) y una débil disminución de mapa de $M_x: \mathbb{Z} \longrightarrow \mathbb{N}$. La noción de "$x$ es un número real" implica:
$$ \left( x \in \mathbb{R} \right) \triangleq \left( \forall k \forall n,m \geq M_x(k) . \big| x(n) - x(m) \big| \leq 2^{-k} \right) $$
Eso significa que $x$ es una secuencia de Cauchy con el módulo de $M_x$.
- Apartness de dos números reales se define como:
$$ \left( x \neq y \right) \triangleq \left( \exists k \forall n \geq \max \{ M_x(k), M_y(k) \} . \big| x(n) - y(n) \big| \geq 2^{-k} \right) $$
lo que implica un testimonio $k$ que necesita ser construida en cada caso en particular.
Ahora, un (uniformemente continua) de la función en los números reales $ f: [a, b] \longrightarrow \mathbb{R}, a,b \in \mathbb{Q} $ es una tupla que consta de:
- Un mapa de $h_f: [a, b] \cap \mathbb{Q} \times \mathbb{N} \longrightarrow \mathbb{Q}$ s. t. $ \{ h_f(c, n) \}_n $ es una secuencia de Cauchy con el módulo de $ \alpha_f $
- Un mapa de $\omega_f: \mathbb{Z} \longrightarrow \mathbb{N}$ s. t.
$$ \forall k \forall n \geq \alpha_f(k) . \left( |p - q| \leq 2^{ - \omega_f(k) + 1 } \Rightarrow | h_f(p, n) - h_f(q, n) | \leq 2^{-k}\right) $$
El mapa de $h_f$ se llama la aproximación del mapa de $f$ $\omega_f$ es el módulo de la continuidad de $f$.
- Una función de $ f: [a, b] \longrightarrow \mathbb{R}, a,b \in \mathbb{Q} $ es densamente aparte de un número real $y$ si en cada subinterval (con racional de los extremos), existe un racional $s$ s. t. $f(s)$ es aparte de $y$.
Pregunta: cómo activar esta definición en un algoritmo? Traté de figura con funciones simples, como exponencial y no puede realmente de entender.
Por ejemplo, si dejo $y=\sqrt{2}$ se define como aquí y una función de $f(x) = e^x$ con el conocido aproximación:
$$ h_f(c, n) := \sum_{l=0}^{n} \frac{ c^l }{ l! } $$
(De Cauchy y la continuidad de los módulos son fácilmente derivable) cómo venir para arriba con un algoritmo de tomar dos racionales como entrada y en realidad encontrar un racional $s$ y un entero $k$ presenciando $e^s \neq \sqrt{2} $? Todo lo que he intentado resultó ser circular o heurística. Mientras tanto, este importante concepto se utiliza para definir locales no constancia que es aún más complicada ya que implica un algoritmo de tomar no sólo los extremos de un intervalo, pero también un número real, y casi todos los cálculos pueden ser recuperados en base a esto.
También me gustaría, realmente aprecio mucho si alguien pudiera arrojar algo de luz sobre la actualización a esta pregunta.
Así que aquí están los datos para la función exponencial en un intervalo de $[a, b]$:
- Cauchy módulo se define por la condición:
$$ \Bigg| \sum_{l=0}^{n} \frac{s^l}{l!} - \sum_{l=0}^{m} \frac{s^l}{l!} \Bigg| \leq 2 \frac{|s|^{n+1}}{(n+1)!}, s \in \mathbb{Q}, |s| \leq 1 + \frac{n}{2} $$
- La continuidad del módulo se define por la condición:
$$ \Bigg| \sum_{l=0}^{n} \frac{s^l}{l!} - \sum_{l=0}^{n} \frac{r^l}{l!} \Bigg| \leq |s-r| e^{ \max\{ |a|, |b| \} }, s,r \in \mathbb{Q} $$
De ello se desprende que la búsqueda de un racional $s$ en algunos subinterval $[p, q]$ s. t. $e^s \neq y$ donde $y$ es un hecho real asciende a encontrar este tipo de productos naturales $n, m, n \geq m$ que:
$$ \sum_{l=0}^{n} \frac{q^l}{l!} - \frac{|q|^{n+1}}{(n+1)!} - \sum_{l=0}^{m} \frac{p^l}{l!} - \frac{|p|^{m+1}}{(m+1)!} > 2^{-k+1}$$
donde $k$ es natural. Después de algunas manipulaciones, me reformular el problema en términos de:
$$ \sum_{l=0}^{n-1} \frac{q^l - p^l}{l!} - \frac{p^n}{n!} > 2^{-k+1}$$
incluso para $n$.
