\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{continued fraction}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{coalgebraic_formulation}{Coalgebraic formulation}\dotfill \pageref*{coalgebraic_formulation} \linebreak
\noindent\hyperlink{topology_of_infinite_continued_fractions}{Topology of infinite continued fractions}\dotfill \pageref*{topology_of_infinite_continued_fractions} \linebreak
\noindent\hyperlink{examples_and_further_results}{Examples and further results}\dotfill \pageref*{examples_and_further_results} \linebreak
\noindent\hyperlink{half-open}{Reals as terminal coalgebra}\dotfill \pageref*{half-open} \linebreak
\noindent\hyperlink{rationals_as_initial_algebra}{Rationals as initial algebra}\dotfill \pageref*{rationals_as_initial_algebra} \linebreak
\noindent\hyperlink{rational_tangles}{Rational tangles}\dotfill \pageref*{rational_tangles} \linebreak
\noindent\hyperlink{the_calkinwilf_and_sternbrocot_trees}{The Calkin-Wilf and Stern-Brocot trees}\dotfill \pageref*{the_calkinwilf_and_sternbrocot_trees} \linebreak
\noindent\hyperlink{constructive_aspects}{Constructive aspects}\dotfill \pageref*{constructive_aspects} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \emph{continued fraction} (\emph{Kettenbr\"u{}che} in German) is a finite or infinite expression of the form

\begin{displaymath}
x = a_0 + \frac{b_1}{a_1 + \frac{b_2}{a_2 + \frac{b_3}{a_3 + \cdots}}}
\end{displaymath}
with convergence under appropriate conditions. The most commonly used form is where $b_i = 1$ for all $i$; such is called a \emph{regular} continued fraction.

Every real number may be (more or less\footnote{For rational numbers, there are two continued fraction representations, agreeing up to say $a_{n-1}$, but ending with $a_n \gt 1$ in one case and $a_n - 1, a_{n+1} = 1$ in the other (since after all $a_n = (a_n - 1) + 1/1$). This can be an annoyance, but there are various workarounds.} ) uniquely expressed as a finite or infinite regular continued fraction for which all the $a_i$ are [[integers]] and $a_i \gt 0$ for $i \gt 0$. The expression is an infinite continued fraction if and only if the real number is [[irrational number|irrational]], so that there is a [[bijection]]

\begin{displaymath}
\mathbb{Z} \times (\mathbb{N}_+)^{\mathbb{N}_+} \to \{irrationals\}
\end{displaymath}
\begin{displaymath}
(a_0; a_1, a_2, \ldots) \mapsto x = a_0 + \frac{1}{a_1 + \frac{1}{a_2 + \frac{1}{a_3 + \cdots}}}.
\end{displaymath}
This is in fact a [[homeomorphism]] if we endow the left side with the [[product topology]] and the right side with the [[subspace]] topology, regarding the set of irrationals as a subset of the real line (with its standard [[topological space|topology]]). (The space of irrationals becomes in this way a kind of prototypical chaotic dynamical system, where the dynamics on the product space is given by a shift map.)

\hypertarget{coalgebraic_formulation}{}\subsection*{{Coalgebraic formulation}}\label{coalgebraic_formulation}

We can describe the basic theory of continued fractions for real numbers in terms of dynamics of [[fractional linear transformations]] on the real [[projective line]] $\mathbb{P}^1(\mathbb{R})$, with the point at infinity playing a special role. From an nPOV, it is useful to cast this in [[coalgebra of an endofunctor|coalgebraic]] terms.

Let us denote by $\mathbf{R}$ the [[interval]] $[1, \infty]$ (considered as a subset of the projective line $\mathbb{P}^1(\mathbb{R})$); if $1 \leq x \lt \infty$, we let $fl(x)$ be the floor of $x$ (the greatest integer such that $fl(x) \leq x$). We denote by $\mathbb{N}_+$ the set of positive integers (so, excluding $0$). Put $\mathbf{1} = \{\ast\}$, and define a map

\begin{displaymath}
\alpha: \mathbf{R} \to \mathbf{1} + \mathbf{R} \times \mathbb{N}_+
\end{displaymath}
where $\alpha(x) = ((x - fl(x))^{-1}, fl(x))$ if $x \lt \infty$, and $\alpha(\infty) = \ast$. This defines a coalgebra of the functor $F: Set \to Set$ defined by the formula

\begin{displaymath}
F(X) = \mathbf{1} + X \times \mathbb{N}_+.
\end{displaymath}
Let us define $x \in \mathbf{R}$ to be \emph{rational} if it is a quotient of two integers (including $0$, so $1/0 = \infty$ is here considered ``rational''). Define $\tau: \mathbf{R} \to \mathbf{R}$ by $\tau(x) = (x - fl(x))^{-1}$ if $x \lt \infty$, and $\tau(\infty) = \infty$.

\begin{lemma}
\label{rational}\hypertarget{rational}{}
An element $x \in \mathbf{R}$ is rational if and only if there exists $n \geq 0$ such that $\tau^n(x) = \infty$.

\end{lemma}
\begin{proof}
Only if: this is clear for $x = \infty$. Otherwise, write $x = p/q$ in lowest terms, so that $p, q \gt 0$ and $\gcd(p, q) = 1$. We argue by strong induction on $q$, where we have $p = n q + r$ for which $n = fl(p/q)$ and $0 \leq r \lt q$ by the Euclidean algorithm. If $r = 0$, then $\tau(x) = \infty$ and we are done; otherwise $\tau(p/q) = q/r$ where $q \gt r \gt 0$ and $\gcd(q, r) = 1$, whence $\tau^n (q/r) = \infty$ for some $n$ by inductive hypothesis, and then $\tau^{n+1}(p/q) = \infty$.

If: argue by induction on the least $n$ such that $\tau^n(x) = \infty$. If $n = 0$, then $x = \tau^0(x) = \infty$ is rational. Otherwise, we have

\begin{displaymath}
x = fl(x) + 1/\tau(x)
\end{displaymath}
and since $\tau^{n-1}(\tau(x)) = \infty$, we have that $\tau(x)$ is rational by inductive hypothesis, and therefore $x$ is also rational.

\end{proof}
\begin{lemma}
\label{converge}\hypertarget{converge}{}
If $(a_0, a_1, a_2, \ldots) \in (\mathbb{N}_+)^{\mathbb{N}}$ is any sequence of positive integers, then there is a unique $x \in \mathbf{R}$ such that $a_n = fl(\tau^n(x))$ for all $n \geq 0$. (This $x$ must be irrational by Lemma \ref{rational}.)

\end{lemma}
\begin{proof}
In a nutshell, $x$ is given by the continued fraction

\begin{displaymath}
x = a_0 + \frac{1}{a_1 + \frac{1}{a_2 + \frac{1}{a_3 + \cdots}}}
\end{displaymath}
and so it is really only a matter of proving that this continued fraction converges, i.e., that its truncations $p_n/q_n = [a_0, a_1, \ldots, a_n]$, namely the rational numbers $p_n/q_n$ with $\tau^{n+1}(p_n/q_n) = \infty$ and $fl(\tau^k(p_n/q_n)) = a_k$ for $0 \leq k \leq n$, form a [[Cauchy sequence]].

For $a \in \mathbb{N}_+$, let $a \cdot -: \mathbf{R} \to \mathbf{R}$ denote the fractional linear transformation $x \mapsto a + \frac1{x}$. We have

\begin{displaymath}
[a] = a \cdot \infty, \qquad [a_0, a_1, \ldots, a_n] = a_0 \cdot [a_1, \ldots, a_n]
\end{displaymath}
and since $a \cdot -: \mathbf{R} \to \mathbf{R}$ is monotone decreasing, we have that $a_0 \cdot (a_1 \cdot -)$ is monotone increasing. Thus some easy inductions establish

\begin{itemize}%
\item \begin{displaymath}
[a_0] \lt [a_0, a_1, a_2] \lt [a_0, a_1, a_2, a_3, a_4] \lt \ldots
\end{displaymath}

\item \begin{displaymath}
[a_0, a_1] \gt [a_0, a_1, a_2, a_3] \gt [a_0, a_1, a_2, a_3, a_4, a_5] \gt \ldots
\end{displaymath}

\item \begin{displaymath}
[a_0, \ldots, a_{2n}] \lt [a_0, \ldots, a_{2n}, a_{2n+1}]
\end{displaymath}


\end{itemize}
so that $\sup_n [a_0, \ldots, a_{2n}] \leq \inf_n [a_0, \ldots, a_{2n+1}]$, and all that remains is to show $lim_{m\to \infty} {|p_m/q_m - p_{m+1}/q_{m+1}|} = 0$.

In fact we have

\begin{displaymath}
\left|\frac{p_m}{q_m} - \frac{p_{m+1}}{q_{m+1}}\right| = \frac{{|p_m q_{m+1} - p_{m+1}q_m|}}{q_m q_{m+1}} = \frac1{q_m q_{m+1}}
\end{displaymath}
The second equation is proved by induction on the length $j$ of continued fraction representations $[x_1, \ldots, x_j]$. Put $[a_1, \ldots, a_m] = \frac{q_m}{r_m}$ and $[a_1, \ldots, a_{m+1}] = \frac{q_{m+1}}{r_{m+1}}$, with all fractions in reduced form, and suppose as induction hypothesis that ${|q_m r_{m+1} - q_{m+1}r_m|} = 1$. The fractional linear transformation $a_0 \cdot -$, being represented by the integral [[matrix]]

\begin{displaymath}
A_0 = \left(
\itexarray{ 
a_0 & 1 \\
1 & 0
}\right)
\end{displaymath}
with [[determinant]] $-1$, takes $(\pm 1)$-determinant matrices to $(\pm 1)$-determinant matrices. In particular it takes the determinant of absolute value $1$ on the left to one on the right,

\begin{displaymath}
\left(
\itexarray{
q_m & q_{m+1} \\
r_m & r_{m+1}
}\right) \; \; \stackrel{A_0}{\mapsto} \; \; \left(
\itexarray{
p_m & p_{m+1} \\
q_m & q_{m+1}
}\right),
\end{displaymath}
and this completes the induction.

Here $p_m = a_0 q_m + r_m \gt 2r_m$ and $p_{m+1} = a_0 q_{m+1} + r_{m+1} \gt 2r_{m+1}$. Similarly, if

\begin{displaymath}
[a_2, \ldots, a_m] = \frac{r_m}{s_m}, \qquad [a_2, \ldots, a_{m+1}] = \frac{r_{m+1}}{s_{m+1}},
\end{displaymath}
then $q_m \gt 2s_m$ and $q_{m+1} \gt 2s_{m+1}$. Thus we have

\begin{itemize}%
\item \begin{displaymath}
{|[a_2, \ldots, a_m] - [a_2, \ldots, a_{m+1}]|} = \frac1{s_m s_{m+1}}
\end{displaymath}

\item \begin{displaymath}
{[a_0, \ldots, a_m] - [a_0, \ldots, a_{m+1}]|} = \frac1{q_m q_{m+1}} \lt \frac1{(2s_m)(2s_{m+1})} = \frac1{4s_m s_{m+1}}
\end{displaymath}


\end{itemize}
so that by induction, ${|p_{2m}/q_{2m} - p_{2m+1}/q_{2m+1}|} \leq \frac1{4^m}$, completing the proof that the infinite continued fraction converges.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
It may be tempting to believe that this $F$-coalgebra structure makes $\mathbf{R}$ the terminal coalgebra. That is unfortunately not correct because the coalgebra structure $\xi: \mathbf{R} \to F(\mathbf{R})$ is not an isomorphism (it fails to be surjective because no element maps to $(1, 1, \infty)$ under $\xi$; this is the fact that the standard continued fraction for $2$ is just $2$ and not $1 + 1/1$). However, \hyperlink{half-open}{below} we will exhibit a different kind of coalgebra making half-open intervals a terminal coalgebra.

\end{remark}
\hypertarget{topology_of_infinite_continued_fractions}{}\subsection*{{Topology of infinite continued fractions}}\label{topology_of_infinite_continued_fractions}

Let $\mathbf{I}$ be the set of irrational elements $x \in \mathbf{R}$. The results above imply that $\mathbf{I}$ equipped with the map

\begin{displaymath}
\mathbf{I} \to \mathbf{I} \times \mathbb{N}_+: x \stackrel{\alpha}{\mapsto} ((x - fl(x))^{-1}, fl(x))
\end{displaymath}
is a terminal coalgebra for the functor $- \times \mathbb{N}_+: Set \to Set$, isomorphic to $(\mathbb{N}_+)^{\mathbb{N}}$ under the coalgebra structure

\begin{displaymath}
(\mathbb{N}_+)^{\mathbb{N}} \stackrel{(\mathbb{N}_+)^{\langle s, o\rangle}}{\to} (\mathbb{N}_+)^{\mathbb{N} + \mathbf{1}} \cong (\mathbb{N}_+)^\mathbb{N} \times \mathbb{N}_+.
\end{displaymath}
Endow $\mathbf{I}$ with the subspace topology coming from $\mathbf{R}$ (as one-point [[compactification]] of $[1, \infty)$), and $(\mathbb{N}_+)^{\mathbb{N}}$ with the topology of the [[product]] of countably many [[discrete spaces]] $\mathbb{N}$.

\begin{lemma}
\label{}\hypertarget{}{}
The coalgebra isomorphism $\mathbf{I} \to (\mathbb{N}_+)^{\mathbb{N}}$ is a [[continuous map]].

\end{lemma}
\begin{proof}
It suffices to check that each composite

\begin{displaymath}
\mathbf{I} \to (\mathbb{N}_+)^{\mathbb{N}} \stackrel{\pi_n}{\to} \mathbb{N}_+
\end{displaymath}
is continuous. Following the notation $\tau(x) = (x - fl(x))^{-1}$ above, this composite map is $x \mapsto fl(\tau^n(x))$, so it suffices to check that $fl: \mathbf{I} \to \mathbb{N}_+$ is continuous, or in other words that

\begin{displaymath}
\{x \in \mathbf{I}: fl(x) = m\}
\end{displaymath}
is [[open set|open]] for every $m$. This set is clearly open, being the intersection $(m, m+1) \cap \mathbf{I}$ (noting that of course $m \notin \mathbf{I}$!).

\end{proof}
\begin{lemma}
\label{}\hypertarget{}{}
The coalgebra isomorphism $\psi: (\mathbb{N}_+)^{\mathbb{N}} \to \mathbf{I}$ is continuous.

\end{lemma}
\begin{proof}
This merely says that for each sequence of positive integers $(a_0, a_1, \ldots)$ and for a given $\epsilon \gt 0$, that there exists $N$ such that ${|\psi(a_0, a_1, \ldots) - \psi(b_0, b_1, \ldots)|} \lt \epsilon$ provided $a_i = b_i$ for $i = 0, \ldots, N$. But this just follows the proof of convergence of continued fractions given in the proof of Lemma \ref{converge}.

\end{proof}
\begin{corollary}
\label{}\hypertarget{}{}
The coalgebra isomorphism $\psi$ is a homeomorphism.

\end{corollary}
This makes the space of irrationals $\mathbf{I}$ the terminal coalgebra for the endofunctor $- \times \mathbb{N}_{+}: Top \to Top$.

\hypertarget{examples_and_further_results}{}\subsection*{{Examples and further results}}\label{examples_and_further_results}

\begin{example}
\label{}\hypertarget{}{}
A continued fraction $[a_0, a_1, \ldots]$ is periodic, i.e., satisfies $a_i = a_{k+i}$ for some fixed $k$ and all $i$, only if it is the root of a quadratic equation $a_0 \cdot (a_1 \cdot \ldots (a_{k-1} \cdot x)\ldots ) = x$ (where the operator on the left can be written as a fractional linear transformation). Every quadratic irrational is \emph{eventually} periodic (i.e., for some $k$ and $N$ we have $a_i = a_{k+i}$ for all $i \geq N$): the proof is part of the theory of [[Pell's equation]].

\end{example}
This example shows that periodic points are [[dense subset|dense]] in the discrete [[dynamical system]] $\alpha^{-1}: \mathbf{I} \times \mathbb{N}_+ \to \mathbf{I}$, since quadratic surds are dense among all irrationals.

Part of the story of Pell's equation is that an integer solution to $x^2 - D y^2 = \pm 1$, with $D$ is a square-free integer, is a pair $(x, y) = (p, q)$ where $p/q$ is a reduced form fraction (a rational approximant) represented by a finite truncation of the continued fraction of $\sqrt{D}$.

\begin{example}
\label{}\hypertarget{}{}
The quadratic irrational represented by $[1, 1, 1, \ldots]$ is the [[golden ratio]] $\Phi = \frac1{2}(1 + \sqrt{5}) \approx 1.618\ldots$. Many properties of this constant (as manifested both mathematically and physically) are due to this fact and the fact that of all infinite continued fractions, the convergence rate of its rational approximants is slowest for this number.

\end{example}
\begin{remark}
\label{}\hypertarget{}{}
Were the Pythagoreans the first to do coalgebra? John Baez remarks in \href{http://math.ucr.edu/home/baez/week265.html}{Week 265} that the Pythagoreans were fascinated by pentagrams, and drops hints that they may have been aware of the continued fraction for the golden ratio and also the fact that $\Phi$ is irrational. The Pythagorean pentagram on display in Baez's page clearly indicates an infinite stream of pentagons which can be viewed as a coalgebraic behavior stream. And indeed if $\Phi$ were a rational number $p/q$ with $p, q$ as small as possible, then we would also have $\Phi = q/(p-q)$, with numerator and denominator even smaller, contradiction. This is analogous to one of the famous proofs of irrationality of $\sqrt{2}$: if $\sqrt{2} = p/q$, then also $\sqrt{2} = (2q - p)/(p-q)$, which generates an infinite descending stream of positive numerators and denominators, contradiction.

\end{remark}
\begin{example}
\label{}\hypertarget{}{}
The continued fraction for [[Euler's number]] [[e]] is given by

\begin{displaymath}
[2, 1, 2, 1, 1, 4, 1, 1, 6, 1, 1, 8, \ldots].
\end{displaymath}
A proof may be found \href{http://topologicalmusings.wordpress.com/2008/08/04/continued-fraction-for-e/}{here}.

\end{example}
\begin{example}
\label{}\hypertarget{}{}
The regular continued fraction for [[pi|Ludolph's number]] $\pi$ displays no regularity, but other types of continued fractions do. See \href{http://en.wikipedia.org/wiki/Pi#Continued_fractions}{Wikipedia}.

\end{example}
The popularity of certain rational approximations to [[pi]] such as $\frac{22}{7}$ or $\frac{355}{113}$ can be explained by the fact that these are rational approximants obtained by truncating the regular continued fraction for $\pi$, coupled with the following result.

\begin{theorem}
\label{}\hypertarget{}{}
The truncation $p/q = [a_0, a_1, \ldots, a_n]$ is a ``best'' rational approximant to the irrational number $\beta = [a_0, a_1, \ldots]$, in the sense that it minimizes the distance to $\beta$ among all rational numbers $r/s$ whose denominators $s$ are less than or equal to $q$.

\end{theorem}
The space of irrationals $\mathbf{I}$ may be identified with the space of irrationals in the interval $(0, 1)$ (by taking their reciprocals). Here the action $\alpha^{-1}: Irr(0, 1) \times \mathbb{N} \to Irr(0, 1)$ is generated by the shift map $\tau: x \mapsto x^{-1} \; mod \; 1$.

\begin{theorem}
\label{}\hypertarget{}{}
The map $\tau$ is topologically mixing. Moreover, if $Irr(0, 1)$ is equipped with the [[probability measure]]

\begin{displaymath}
\mu(I) = \frac1{\log 2} \int_I \frac{d x}{1+x},
\end{displaymath}
then $\tau$ is an [[ergodic transformation]] with respect to $\mu$, making $(Irr(0, 1), \tau, \mu)$ an ergodic system.

\end{theorem}
A proof may be found \href{http://www.mathematik.uni-wuerzburg.de/~christ/nihon.pdf}{here}.

\hypertarget{half-open}{}\subsubsection*{{Reals as terminal coalgebra}}\label{half-open}

Returning to the theme of coalgebras, an alternative form of continued fractions may be used to exhibit a half-open real interval as a terminal coalgebra. The alternative continued fractions are of the form

\begin{displaymath}
x = a_0 - \frac{1}{a_1 - \frac{1}{a_2 - \frac{1}{a_3 - \cdots}}}
\end{displaymath}
where the $a_i$ are suitable integers; for now we will call them \emph{antiregular} continued fractions (not knowing what others call them), or acf's for short. These acf's correspond to [[fractional linear transformations]] belonging to $PSL_2(\mathbb{Z})$, generated by the transformations $z \mapsto -1/z$, $z \mapsto z-n$.

Consider the linear order $\mathbb{R}_{\geq 1}$ (this time excluding $\infty$); let $\beta(x)$ be the smallest integer \emph{strictly} greater than $x$.

Consider the endofunctor $G$ on the category of [[linearly ordered sets]] $X$ where $G(X)$ is the set $\mathbb{N} \times X$ equipped with the ordinal product or [[lexicographic order]]. (Actually we replace $\mathbb{N}$ with the set of integers greater than or equal to $2$.) Define a map

\begin{displaymath}
\xi: \mathbb{R}_{\geq 1} \to \mathbb{N}_{\geq 2} \times \mathbb{R}_{\geq 1}
\end{displaymath}
where $\xi(x) = (\beta(x), -\frac1{x - \beta(x)})$.

\begin{theorem}
\label{PavPratt}\hypertarget{PavPratt}{}
\textbf{(\hyperlink{PP}{Pavlovic-Pratt})} The map $\xi$ defines a $G$-coalgebra structure $\xi: \mathbb{R}_{\geq 1} \to G(\mathbb{R}_{\geq 1})$, making $\mathbb{R}_{\geq 1}$ the terminal $G$-coalgebra.

\end{theorem}
\hypertarget{rationals_as_initial_algebra}{}\subsubsection*{{Rationals as initial algebra}}\label{rationals_as_initial_algebra}

Now let $\mathbf{Q} = \{r \in \mathbb{Q}: r \gt 1\} \cup \{\infty\}$, the set of rational elements of $\mathbf{R}$. On the category of linear orders, let $H$ be the endofunctor $H(X) = G(X) + 1$, the [[ordinal sum]] where $G$ was defined \hyperlink{half-open}{above}.

The initial $H$-algebra is the free monoid $\mathbb{N}_+^\ast$, [[lexicographic order|lexicographically ordered]] according to the convention given in this \href{/nlab/show/lexicographic+order#antidictionary}{remark} (where initial segments of words $w$ are \emph{greater} than $w$).

On the other hand, we have an $H$-algebra structure on $\mathbb{Q}$, a function

\begin{displaymath}
\xi:\; (\mathbb{N}_+ \times \mathbf{Q}) + 1 \to \mathbf{Q}
\end{displaymath}
where for $\ast \in 1$, $\xi(\ast) = \infty$, otherwise $\xi(n, r) = n+1-1/r$. Observe that this is indeed a monotone map between the linear orders $H(\mathbf{Q}) \to \mathbf{Q}$.

\begin{theorem}
\label{initial}\hypertarget{initial}{}
$(\mathbf{Q}, \xi)$ is the initial $H$-algebra.

\end{theorem}
The inverse map $\xi^{-1}: \mathbf{Q} \to H(\mathbf{Q})$ is in essence another form of the acf (see above): if $ceil(s)$ denotes the least integer greater than or equal to $s$, then $\xi^{-1}(\infty) = \ast$, and otherwise

\begin{displaymath}
\xi^{-1}(r) = (ceil(r) - 1, -1/(r - ceil(r)).
\end{displaymath}
The $H$-algebra isomorphism $\mathbb{N}_+^\ast \to \mathbf{Q}$ takes a finite word $a_0 a_1 \ldots a_n$ to the rational number to which the acf

\begin{displaymath}
a_0 + 1 - \frac{1}{a_1 + 1 - \frac{1}{a_2 + 1 - \frac{1}{a_3 + 1 - \cdots}}}
\end{displaymath}
evaluates.

\hypertarget{rational_tangles}{}\subsection*{{Rational tangles}}\label{rational_tangles}

Among the many uses of continued fractions, we mention a quite remarkable one due to John H. Conway.

\begin{defn}
\label{}\hypertarget{}{}
A \emph{rational tangle} is a subspace $T$ of the 3-disk $D^3$ obtained by embedding two arcs

\begin{displaymath}
(\alpha_1, \alpha_2): I + I \to D^3,
\end{displaymath}
with endpoints on the boundary $\partial D^3$, such that the pair of spaces $(D^3, T = \alpha_1(I) + \alpha_2(I))$ is homeomorphic to the pair $(D^2 \times I, \{x, y\} \times I)$, with $x, y \in D^2$ distinct points. Two rational tangles $S, T$ are \emph{isotopic} if there exists an orientation-preserving homeomorphism $(D^3, S) \to (D^3, T)$ that is the identity on $\partial D^3$.

\end{defn}
Conventionally, rational tangles (or more general 2-tangles) are exhibited by tangle diagrams placed within a disk (with appropriate over- and under-crossings), say a unit disk ${|z|} \leq 1$ in the complex plane, with endpoints situated at primitive $8^{th}$ roots of unity $\exp((2k+1)i\pi/8)$; these endpoints are indicated by their directions NE, NW, SW, SE. There is a trivial 2-tangle with a chord from NE to NW and another from SE to SW; this is denoted $[0]$. Two operations that can be used to generate further 2-tangles are

\begin{itemize}%
\item ``Turn'' (rotate the disk through 90 degrees counterclockwise),


\item ``Twist'' (insert a ``horizontal'' twist that interchanges NE and SE, which can be a positive twist or a negative twist depending on convention).



\end{itemize}
\begin{theorem}
\label{}\hypertarget{}{}
\textbf{(Conway)} The set of isotopy classes of rational tangles is in bijection with the set of rational elements $q \in \mathbb{Q} \cup \{\infty\}$, in such a way that if $[q]$ is the isotopy class corresponding to $q$, then $[-1/q]$ is the class corresponding to a turn of $[q]$, and $[1+q]$ is the class corresponding to a positive twist of $[q]$.

\end{theorem}
In particular, every rational tangle can be brought back to the trivial tangle $[0]$ by a series of (positive) twists and turns, and every rational tangle is isotopic to the tangle obtained by applying a 180 degree counterclockwise turn to it. A very readable account of this result may be found in an article by Kauffman and Lambropoulou, \href{http://arxiv.org/pdf/math/0311499.pdf}{here}.

It should be remarked that the twist and turn operations correspond to group elements in $PSL_2(\mathbb{Z})$ (cf. the article [[Moebius transformation]], in particular the remarks on the surjective homomorphism $B_3 \to PSL_2(\mathbb{Z})$ where $B_3$ is the braid group on $3$ strands):

\begin{displaymath}
turn = \left(
\itexarray{
0 & 1 \\
-1 & 0
}\right), \qquad pos.twist = \left(
\itexarray{
1 & 1 \\
0 & 1
}\right)
\end{displaymath}
John Baez asks a question about this in \href{http://math.ucr.edu/home/baez/week228.html}{TWF228}, and reports on an answer in \href{http://math.ucr.edu/home/baez/week229.html}{TWF229}. He returns to this topic in an illuminating comment \href{http://golem.ph.utexas.edu/category/2014/04/the_modular_flow_on_the_space.html#c046316}{here}.

David Corfield speculates at the \href{http://golem.ph.utexas.edu/category/2011/01/coalgebraic_tangles.html}{Caf\'e{}} that the infinite tangles mentioned by \hyperlink{KL}{Kauffman and Lambropoulou}, as limits of rational tangles, might be viewed as belonging to a coalgebraic completion of the collection of rational tangles (along the lines of seeing the terminal coalgebra $\mathbf{R}$ as a coalgebraic completion of the initial algebra $\mathbf{Q}$, as in Theorem \ref{initial}).

\hypertarget{the_calkinwilf_and_sternbrocot_trees}{}\subsection*{{The Calkin-Wilf and Stern-Brocot trees}}\label{the_calkinwilf_and_sternbrocot_trees}

The Calkin-Wilf tree is an infinite complete binary tree whose vertices are in 1-to-1 correspondence with the positive rational numbers. The tree may be defined inductively by the following very simple recipe (Calkin \& Wilf, 2000):

\begin{itemize}%
\item $1/1$ is at the top of the tree, and
\item each vertex $i/j$ has two children: its left child is $i/(i+j)$ and its right child is $(i+j)/j$

\end{itemize}
For example, the first four levels of the Calkin-Wilf tree are:

\begin{displaymath}
\frac{1/1}{
 \frac{1/2}{
  \frac{1/3}{1/4\quad 4/3}
  \quad
  \frac{3/2}{3/5\quad 5/2}}
 \quad
 \frac{2/1}{
  \frac{2/3}{2/5\quad 5/3}
  \quad
  \frac{3/1}{3/4\quad 4/1}}}
\end{displaymath}
Remarkably, every positive rational number appears exactly once in the tree, and so performing a breadth-first traversal ($1/1, 1/2, 2/1, 1/3, 3/2, \dots$) gives an enumeration of the positive rationals with no double-counting. In fact, Calkin and Wilf proved that the $n$th number in this sequence is equal to

\begin{displaymath}
\frac{b(n)}{b(n+1)}
\end{displaymath}
where $b(n)$ is the number of ways of writing the integer $n$ as a sum of powers of 2, each power being used at most twice.

By locating a positive rational $q$ in the Calkin-Wilf tree and describing the path to $q$ from the root as a sequence of binary choices, one generates a string of bits which may be interpreted as an ``uncompressed'' representation of the continued fraction of $q$. In turn, compressing this path by counting the number of repeated bits (i.e., by performing a ``run-length encoding'') is a way of reconstructing the continued fraction. This is perhaps easier to see if we first express the two operations returning the left and right children of a vertex $x$ equivalently as

\begin{displaymath}
\begin{aligned}
L(x) &= \frac{1}{1 + \frac{1}{x}} \\
R(x) &= 1 + x
\end{aligned}
\end{displaymath}
from which it follows that

\begin{displaymath}
\begin{aligned}
L^a(x) &= \frac{1}{a + \frac{1}{x}} \\
R^a(x) &= a + x
\end{aligned}
\end{displaymath}
Now, suppose a positive rational $q$ has continued fraction $[a_0,\dots,a_n]$, assuming without loss of generality that $n$ is odd (we allow for $a_n = 1$). Then the path from 1 to $q$ in the Calkin-Wilf tree begins by taking $a_n - 1$ steps to the left, followed by $a_{n-1}$ steps to the right, $a_{n-2}$ steps to the left, and so on, ending with $a_0$ steps to the right. In other words,

\begin{displaymath}
q = R^{a_0}L^{a_1}\dots R^{a_{n-1}} L^{a_n-1} 1
\end{displaymath}
For example:

\begin{displaymath}
\begin{aligned}
2/5 & = LLR(1) = \frac{1}{2 + \frac{1}{1 + 1}} \\
12/7 &= RLRRL(1) = 1 + \frac{1}{1 + \frac{1}{2 + \frac{1}{1 + \frac{1}{1}}}}
\end{aligned}
\end{displaymath}
Finally, the Calkin-Wilf tree gives a simple algebraic characterization of the positive rationals, namely as an initial object in the category of pointed modules for the free monoid on two elements $\{L,R\}$. Given any such module $X$ and point $x \in X$, there is a unique module homomorphism $\mathbb{Q}^+ \to X$ sending $1$ to $x$, defined as follows: given a positive rational $q$, locate $q$ on the Calkin-Wilf tree, and then retrace the path from $1$ to $q$ in $X$, beginning at $x$ and applying the actions $L : X \to X$ and $R : X \to X$ as appropriate.

The Calkin-Wilf tree was first described in a 2000 paper by Neil Calkin and Herbert Wilf, ``Recounting the rationals'', but is closely related to the much older Stern-Brocot tree, another arrangement of the positive rationals with the special property that the values are ordered from left to right. Here are the first four levels of the Stern-Brocot tree:

\begin{displaymath}
\frac{1/1}{
 \frac{1/2}{
  \frac{1/3}{1/4\quad 2/5}
  \quad
  \frac{2/3}{3/5\quad 3/4}}
 \quad
 \frac{2/1}{
  \frac{3/2}{4/3\quad 5/3}
  \quad
  \frac{3/1}{5/2\quad 4/1}}}
\end{displaymath}
In fact, each tree may be obtained from the other by reversing the paths from the root (e.g., $2/5 = LLR(1)$ is reached from the root of the Stern-Brocot tree by going down left twice and then right once).

\hypertarget{constructive_aspects}{}\subsection*{{Constructive aspects}}\label{constructive_aspects}

The construction of a continued fraction from an arbitrary [[real number]] relies on the [[limited principle of omniscience]] to define the [[floor]]; it is not acceptable in [[constructive mathematics]]. Nevertheless, using the usual constructive meaning of [[rational number]] and [[irrational number]] (as well as [[convergence]] in the real numbers), we have that a continued fraction (involving [[natural numbers]]) represents a rational number iff it is finite and an irrational number iff it is infinite; and every rational or irrational number (if positive) is so representable. Constructively, we simply cannot say that every real number is either rational or irrational.

Now, just because a real number has an expansion as a continued fraction, that doesn't mean that it must be rational or irrational. In general, a continued fraction expansion (according to the coalgebraic formulation) is given by a [[stream]] of natural numbers, and a stream is not necessarily finite (so a [[list]]) or infinite (so a [[sequence]]). However, a stream that is not finite must be infinite; accordingly, a real number that is not rational must be irrational \emph{if} it has a continued fraction; even this is not constructively valid without the continued fraction.

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Wikipedia, \emph{\href{http://en.wikipedia.org/wiki/Continued_fraction}{Continued fraction}}


\item Claude Brezinski, \emph{Continued fractions and Pad\'e{} approximants}, North-Holland 1991. (\href{http://www.amazon.com/Continued-Fractions-Pade-Approximants-Brezinski/dp/0444881697}{vendor})


\item A. Ya. Khinchin, \emph{Continued fractions}, U. Chicago Press 1964.


\item Ilan Vardi, \emph{Continued fractions from Euclid to the present day}, unpublished manuscript (\href{http://chronomaitre.org/ContinuedFractions.pdf}{web})


\item [[Louis Kauffman]] and Sofia Lambropoulou, \emph{On the classification of rational tangles}, arXiv (\href{http://arxiv.org/pdf/math/0311499.pdf}{web}).



\end{itemize}
Dan Piponi wrote a series of posts on his blog ``A Neighborhood of Infinity'', using the programming language Haskell to illustrate some of the connections between continued fractions, rational tangles and linear operators:

\begin{itemize}%
\item Dan Piponi, ``Untangling with Continued Fractions'' (\href{http://blog.sigfpe.com/2008/08/untangling-with-continued-fractions.html}{Part 0}, \href{http://blog.sigfpe.com/2008/08/untangling-with-continued-fractions_16.html}{Part 1}, \href{http://blog.sigfpe.com/2008/08/untangling-with-continued-fractions_23.html}{Part 2}, \href{http://blog.sigfpe.com/2008/08/untangling-with-continued-fractions_31.html}{Part 3}, \href{http://blog.sigfpe.com/2008/09/untangling-with-continued-fractions.html}{Part 4}, \href{http://blog.sigfpe.com/2008/10/untangling-with-continued-fractions.html}{Part 5}).

\end{itemize}
The material on half-open intervals as terminal coalgebras was first given by Pavlovi and Pratt,

\begin{itemize}%
\item [[Dusko Pavlovic]] and [[Vaughan Pratt]], \emph{On coalgebras of real numbers}, Electronic Notes in Theoretical Computer Science, Volume 19 (1999), 103--117. (\href{http://www.sciencedirect.com/science/article/pii/S1571066105802725?np=y}{web})

\end{itemize}
A type-theoretic formalization of the rationals in [[Coq]] based on the Stern-Brocot/Calkin-Wilf representation is described in:

\begin{itemize}%
\item Milad Niqui and Yves Bertot, \emph{QArith: Coq Formalisation of Lazy Rational Arithmetic}, INRIA report RR-5004, November 2003. (\href{http://hal.inria.fr/inria-00077041/}{web})

\end{itemize}
Their library includes two implementations of the field operations: 1. a ``strict'' implementation (in the programming languages sense) in which the operations are performed by first converting continued fractions to ordinary fractions, applying the usual algorithms for arithmetic, and then converting back, and 2. a ``lazy'' implementation operating directly on continued fractions, in which the operations only need to inspect a portion of the input stream in order to determine a portion of the output stream. This latter approach is based on ideas originally due to Gosper:

\begin{itemize}%
\item Bill Gosper, \href{http://hack.org/mc/writings/hackerdom/hakmem/cf.html}{``Continued fraction arithmetic''}, MIT AI, Memo 239 HAKMEM, 1972. (Also described in more detail in \href{http://www.tweedledum.com/rwg/cfup.htm}{this unpublished note}.)

\end{itemize}
[[!redirects continued fractions]]



\end{document}