\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\dashskip}{\strut\enskip{ }}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large a filter semantics for $\infty$}

Michael Beeson\\
San Jos\'e State University

Freek Wiedijk\\
University of Nijmegen

\medskip
Calculemus 2002\\
Marseille, France\\
2002-07-03, 14:00
\end{slide}

\begin{slide}
\sectiontitle{infinity}
\slidetitle{$\infty$ in high school calculus}
$$\begin{array}{l}
\displaystyle
\lim_{x\to\infty} {1\over x + 1}
= {1\over\displaystyle \lim_{x\to\infty} (x + 1)}
= {1\over\displaystyle \lim_{x\to\infty} x + \lim_{x\to\infty} 1}
= {1\over\displaystyle \infty + \lim_{x\to\infty} 1}
\\\noalign{\medskip}\displaystyle
= {1\over\infty + 1}
= {1\over\infty}
= 0
\end{array}$$

\adviwait
calculus textbooks\\
-- avoid this kind of calculation in the explanations\\
-- need this kind of calculation for the exercises
\adviwait

the symbol $\infty$ is confusing to the student:\\
\dashskip infinite limits are\advirecord{dots}{\rlap{ \dots}}\adviplay{dots}%
\adviwait\adviplay[white]{dots}
\begin{tabular}{l}
undefined?\\\adviwait
defined with value $\infty$?
\end{tabular}
\vfill
\end{slide}

\begin{slide}
\slidetitle{$\infty$ in MathXpert}

MathXpert: computer algebra for high school students\\
\adviwait
written by Michael Beeson as a three year research project\\
followed by four years of commercial development
\adviwait

graphs, algebra, trigonometry, limits, differentiation, integration\\
\adviwait
presentation looks exactly like in calculus textbooks\\
\adviwait
correctness through non-standard analysis\adviwait:
completely hidden from user
\adviwait

\medskip
\begin{center}
\begin{tabular}{ccl}
\medskip
$\displaystyle {1\over\infty + 1}$ &$\quad$& \dots\\
\smallskip
$\displaystyle {1\over\infty}$ && \small $\lim u+v = \infty\mbox{ if }u\to\infty\mbox{ and }\lim v\mbox{ is finite}$\\
$\displaystyle 0$ && \small $\lim(u/v) = 0\mbox{ if }\lim u \ne 0\mbox{, }\lim v = \pm\infty$
\end{tabular}
\end{center}
\medskip

\adviwait
Input: \texttt{1/(infinity + 1)}\\
Error: \textcolor{slidegreen}{Input not acceptable: you entered an undefined expression}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{correctness of computer algebra}

tension:
mathematical correctness
$\longleftrightarrow$
doing useful calculations

\adviwait
`too eager' calculations are `repaired' in later versions\\
on an ad hoc basis, to shut up the most blatant criticism

\adviwait
main cause of problems: assumptions are not tracked systematically

\adviwait
\begin{center}
\begin{tabular}{rcl}
\texttt{Sqrt[x${}^{\tt 2}$]\adviwait\ } & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{Sqrt[x${}^{\tt 2}$]\ \ }\\
\adviwait
\texttt{\llap{PowerExpand}[Sqrt[x${}^{\tt 2}$]]} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{x}
\end{tabular}
\end{center}
\textcolor{slidegreen}{Use \texttt{PowerExpand} with caution because \texttt{PowerExpand}
disregards issues of branches of multi-valued functions.}
\adviwait
\begin{center}
\begin{tabular}{rcl}
\texttt{Integrate[Integrate[Sqrt[(x-y)${}^{\tt 2}$],{\char123}x,0,1{\char125}],{\char123}y,0,1{\char125}]} & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{0}
\end{tabular}
\end{center}
\adviwait

\medskip
interfacing TPS with CAS:\\
\dashskip correctness of TPS proofs will be tainted by CAS calculations
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{semantics of computer algebra}
semantics of CAS terms:\\
\dashskip necessary to meaningfully interface CAS and TPS

\adviwait
\begin{center}
\begin{tabular}{rcl}
\texttt{\llap{Integrate}[1/x, x]} & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{Log[x]}
\end{tabular}
\end{center}
\adviwait
no clear semantics for this \texttt{Integrate} on the functional level\\
\adviwait
-- is \texttt{1/x} a number or a function?\\
\adviwait
-- where is the constant of integration?

\adviwait
\textcolor{slidered}{wanted:} uniform semantics for CAS terms\\
\adviwait
difficult because of feature interaction:

\dashskip functional expressions,
constants of integration,
big-Oh notation,
\\\dashskip
\textcolor{slidered}{$\infty$},
undefinedness,
vectors and matrices,
\dots

\vfill
\end{slide}

\begin{slide}
\slidetitle{$\infty$ and interval arithmetic in computer algebra}

\begin{center}
\begin{tabular}{rcl}
\texttt{1/(Infinity + 1)} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{O}\\
\adviwait
\texttt{Sqrt[Infinity]} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & $\infty$\\
\adviwait
\texttt{Infinity - Infinity} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{Indeterminate}\\
\adviwait
\texttt{Sin[Infinity]} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{Interval[{\char123}-1,1{\char125}]}\\
\adviwait
\texttt{1/Interval[{\char123}-1,1{\char125}]} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{Interval[{\char123}-$\infty$,-1{\char125},{\char123}1,$\infty${\char125}]}\\
\adviwait
\texttt{\llap{I}nfinity/Interval[{\char123}-1,1{\char125}]} \adviwait & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{Interval[{\char123}-$\infty$,-$\infty${\char125},{\char123}$\infty$,$\infty${\char125}\rlap{]}}
\end{tabular}
\end{center}

\adviwait
\medskip
Mathematica contains a calculus of three symbols:

\dashskip \texttt{Infinity}\\
\dashskip \texttt{Indeterminate}\\
\dashskip \texttt{Interval}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{filters}
\slidetitle{a filter semantics for $\infty$}

limit values: filter on ${\mathbb R}$
\advirecord{space}{\ $\leftarrow$ underlying topological space}\\
\adviwait
{\setbox0=\hbox{limit values:}\hskip\wd0} $\equiv$ collection of open subsets of ${\mathbb R}$\\
\hbox{}{\setbox0=\hbox{limit values:}\hskip\wd0} {\setbox0=\hbox{$\equiv$}\hskip\wd0} closed under finite $\cap$\\
\hbox{}{\setbox0=\hbox{limit values:}\hskip\wd0} {\setbox0=\hbox{$\equiv$}\hskip\wd0} closed under supersets
\adviwait
\adviplay{space}%
\adviwait

filter $\infty$
$\equiv$ the set of all $U$ such that $U$ contains a neighborhood of $\infty$
\adviwait
$$U \in \infty \iff \exists\, a \in {\mathbb R} : (a,\infty) \subseteq U$$
\begin{itemize}
\adviwait
\item[\footnotesize $\bullet$] for us filters are collections of open sets only
\adviwait
\item[\footnotesize $\bullet$] the two extreme filters are not excluded
\begin{itemize}
\item set of all subsets: `improper' filter
\item empty set of subsets: `empty' filter
\end{itemize}
\end{itemize}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{examples of filters}
\begin{tabular}{rcccl}
$\mbox{\sf{\textcolor{slidegreen}{principal}}}(a)$ & $\equiv$ & $\bar{a}$ & $\equiv$ & $\{ U \,|\, a \in U \}$\\
\quad\rlap{embeds ${\mathbb R}$ in the space of filters}\\
\adviwait
$\mbox{\sf{\textcolor{slidegreen}{punctured}}}(a)$ & $\equiv$ & $a^{\pm}$ & $\equiv$ & \rlap{$\{ U \,|\, \exists\,\varepsilon : (a - \varepsilon,a) \cup (a,a+\varepsilon) \subseteq U \}$}\\
$\mbox{\sf\textcolor{slidegreen}{left}}(a)$ & $\equiv$ & $a^-$ & $\equiv$ & $\{ U \,|\, \exists\,\varepsilon : (a - \varepsilon,a) \subseteq U \}$\\
$\mbox{\sf\textcolor{slidegreen}{right}}(a)$ & $\equiv$ & $a^+$ & $\equiv$ & $\{ U \,|\, \exists\,\varepsilon : (a,a + \varepsilon) \subseteq U \}$\\
\quad\rlap{corresponds to `normal' and `one-sided' limits}\\
\adviwait
$\mbox{\sf\textcolor{slidegreen}{bi-infinity}}$ & $\equiv$ & $\pm\infty$ & $\equiv$ & \rlap{$\{ U \,|\, \exists\,\varepsilon : (-\infty,-1/\varepsilon) \cup (1/\varepsilon,\infty) \subseteq U \}$}\\
\quad\rlap{the filter value of $\displaystyle\lim_{x\to 0} 1/x$}\\
\adviwait
\hbox{}\hspace{-.6em}\rlap{\textbf{error filters}}\hfill\hbox{}\\
$\mbox{\sf{\textcolor{slidegreen}{indeterminate}}}$ & $\equiv$ & $\leftrightarrow$ & $\equiv$ & $\{ {\mathbb R} \}$\\
$\mbox{\sf{\textcolor{slidegreen}{domain-error}}}$ & $\equiv$ & $\bot$ & $\equiv$ & $\emptyset$\\
\vspace{-2em}
$\mbox{\sf\textcolor{slidegreen}{improper}}$ & $\equiv$ & $\dagger$ & $\equiv$ & $\{ U \,|\, U \subseteq {\mathbb R} \}$
\end{tabular}
\vfill
\end{slide}

\begin{slide}
\slidetitle{lifting functions to filters}
sum of two filters $A$ and $B$\\
\adviwait
$\equiv$ filter generated by all $X + Y$ where $X \in A$ and $Y \in B$
\adviwait

\dashskip $X + Y = \{x + y \,|\, x \in X\mbox{, }y \in Y\}$\\
\adviwait
\dashskip the filter generated by a collection of sets $A$ is\\
\dashskip\dashskip $\{U \,|\, \exists\, X \in A : X \subseteq U\}$
\adviwait

\medskip
lifting functions $f$ to filter versions $\bar{f}$\\
\dashskip definition of $\bar{f}$ is analogous to that of $+$ above
\adviwait

term language of CAS also makes sense for filter expressions
\vfill
\end{slide}

\def\Lim{\mathop{\rm Lim}}

\begin{slide}
\slidetitle{refinement}
isn't an infinite limit undefined?\\
\adviwait
solution: the filter \textcolor{slidegreen}{infinity} \textbf{refines} the filter \textcolor{slidegreen}{indeterminate}:
$$\infty\sqsubseteq\mathord{\leftrightarrow}$$

\adviwait
definition of refinement: $A \sqsubseteq B \iff B \subseteq A$ as a set of subsets

\adviwait
examples:
$$\lim_{x\to\infty} \sin x = [-1,1] \sqsubseteq \mathord{\leftrightarrow}$$
\adviwait
$$\lim_{x\to 0} x^2 = 0^+ \sqsubseteq 0^{\pm} \sqsubseteq \bar{0}$$
\adviwait
$$\lim_{x\to 0} {1\over x^2} = {1\over 0^+} = \infty \sqsubseteq {1\over 0^{\pm}} = \pm\infty \sqsubseteq {1\over \bar{0}} = \mathord{\bot}$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{limits to a filter}
two kinds of limit notation:

\dashskip $\displaystyle \lim_{x\to a} {}$ for limits to real numbers\\
\dashskip $\displaystyle \Lim_{x\to A} {}$ for `limits to filters'
\adviwait

correspondence theorem:
%$$\lim_{x\to\infty} f(x) = b \iff \Lim_{x\to\infty} f(x) \sqsubseteq \bar{b}$$
$$\lim_{x\to a} f(x) = b \iff \Lim_{x\to a^{\pm}} f(x) \sqsubseteq \bar{b}$$
use filters to calculate normal limits rigorously!
\adviwait
%$$\Lim_{x\to\infty} {1\over x + 1} \sqsubseteq {\bar{1}\over\displaystyle\Lim_{x\to\infty} (x + 1)} \sqsubseteq {\bar{1}\over\infty + \bar{1}} = {\bar{1}\over\infty} = 0^+ \sqsubseteq \bar{0}$$
$$\Lim_{x\to 0^{\pm}} x \sin {1\over x} \sqsubseteq 0^{\pm} \sin {1\over 0^{\pm}} = 0^{\pm} \sin(\pm\infty) = 0^{\pm} [-1,1] = \bar{0}$$
\adviwait
%$$\mbox{\llap{$\Rightarrow$ }}\lim_{x\to\infty} {1\over x + 1} = 0$$
$$\Rightarrow\;\displaystyle\lim_{x\to 0} x \sin {1\over x} = 0$$
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{interval filters as a uniform notation}

`interval filters'
$$\left\{\begin{array}{cc}(a,b)&(a,b]\\{}[a,b)&{}[a,b]\end{array}\quad\mbox{with}\quad\begin{array}{c}a,b \in \{-\infty\} \cup {\mathbb R} \cup \{\infty\}\\a\le b\end{array}\right\}$$
\adviwait
$=$ `connected filters': filters generated by a set of connected sets
\adviwait

\medskip
uniform way to write many filters\adviwait
$$\begin{array}{c}\bar{a} = [a,a]\\a^- = [a,a)\\a^+ = (a,a]\adviwait\\\advirecord{pm}{a^{\pm} = [a,a) \vee (a,a]}\end{array}\qquad
\begin{array}{c}\infty = [\infty,\infty)\\-\infty = (-\infty,-\infty]\adviwait\\\mathord{\leftrightarrow} = (-\infty,\infty)\adviwait\\\advirecord{bi}{\pm\infty = (-\infty,-\infty] \vee [\infty,\infty)}\end{array}$$
\adviplay{pm}\adviplay{bi}%
$A \vee B$ is the \textbf{join} of two filters $A$ and $B$:
the set of filters is a lattice
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{outlook}
\slidetitle{filters versus Mathematica}
correspondence to Mathematica is not perfect\\
different treatment of domain errors
\adviwait
$$\begin{array}{rcll}
\medskip
\displaystyle \Lim_{x\to\infty} {1\over\sin x}
&=& \displaystyle {1\over[-1,1]} \adviwait = (-\infty,-1] \vee [1,\infty) & \mbox{$\leftarrow$ Mathematica}\\
\adviwait
&=& \displaystyle {1\over[-1,1]} = \bot & \mbox{$\leftarrow$ our definitions}
\adviwait
\end{array}\bigskip$$
\vbox to 0pt{\hbox to \hsize{%
\includegraphics[0,0][136.5,80]{graph3.jpg}%
\hss}\vss}
\hbox{}\hfill $\displaystyle{1\over\sin x}$ undefined at multiples of $\pi$
\vfill
\end{slide}

\begin{slide}
\slidetitle{filters versus non-standard analysis}

non-standard analysis:\\
\dashskip another `calculus with first class infinity'
\adviwait
\begin{center}
\begin{tabular}{ccc}
$\infty$ && $\omega$\\
canonical && not canonical\\
$\infty + 1 = \infty$ && $\omega + 1 \ne \omega$\adviwait\\
\noalign{\medskip}
\textbf{the set of filters} && \textbf{ultrapower model}\\
set of filters && only one filter\\
arbitrary filter && ultrafilter\\
filter of open sets && filter of arbitrary sets
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{filters and ${\mathbb C}$}\adviwait

Mathematica expressions are not real valued but complex valued
\adviwait
\begin{center}
\begin{tabular}{rcl}
\texttt{PowerExpand[Log[-x]]} & \hspace{-.5em}$=$\hspace{-.5em} & \texttt{I $\pi$ + Log[x]}
\end{tabular}
\end{center}\adviwait
\medskip
filter approach works just as well for complex numbers
\adviwait

\medskip
examples of complex filters:
\begin{itemize}
\item[\footnotesize $\bullet$] complex infinity
\item[\footnotesize $\bullet$] infinity along the positive $x$-axis
\item[\footnotesize $\bullet$] limit inside an angular sector $\vert \theta \vert < \pi/4$
\end{itemize}
\vfill
\end{slide}

\end{document}