dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-26 01:15:07 +01:00
parent 0f31e10582
commit 2c51620a56
1 changed files with 81 additions and 53 deletions
Download Patch File Download Diff File Expand all files Collapse all files

134
thesis.tex
View File

@@ -14910,31 +14910,31 @@ data, but a program within the language typically has no access to
this internal representation, and can interact with the value only by this internal representation, and can interact with the value only by
applying it to an argument. applying it to an argument.
Most work in this area to date has focused on computability % Most work in this area to date has focused on computability
differences. One of the best known examples is the \emph{parallel if} % differences. One of the best known examples is the \emph{parallel if}
operation which is computable in a language with parallel evaluation % operation which is computable in a language with parallel evaluation
but not in a typical `sequential' programming % but not in a typical `sequential' programming
language~\cite{Plotkin77}. It is also well known that the presence of % language~\cite{Plotkin77}. It is also well known that the presence of
control features or local state enables observational distinctions % control features or local state enables observational distinctions
that cannot be made in a purely functional setting: for instance, % that cannot be made in a purely functional setting: for instance,
there are programs involving call/cc that detect the order in which a % there are programs involving call/cc that detect the order in which a
(call-by-name) `+' operation evaluates its arguments % (call-by-name) `+' operation evaluates its arguments
\citep{CartwrightF92}. Such operations are `non-functional' in the % \citep{CartwrightF92}. Such operations are `non-functional' in the
sense that their output is not determined solely by the extension of % sense that their output is not determined solely by the extension of
their input (seen as a mathematical function % their input (seen as a mathematical function
$\N_\bot \times \N_\bot \rightarrow \N_\bot$); % $\N_\bot \times \N_\bot \rightarrow \N_\bot$);
%% % %%
however, there are also programs with `functional' behaviour that can % however, there are also programs with `functional' behaviour that can
be implemented with control or local state but not without them % be implemented with control or local state but not without them
\citep{Longley99}. More recent results have exhibited differences % \citep{Longley99}. More recent results have exhibited differences
lower down in the language expressivity spectrum: for instance, in a % lower down in the language expressivity spectrum: for instance, in a
purely functional setting \textit{\`a la} Haskell, the expressive % purely functional setting \textit{\`a la} Haskell, the expressive
power of \emph{recursion} increases strictly with its type level % power of \emph{recursion} increases strictly with its type level
\citep{Longley18a}, and there are natural operations computable by % \citep{Longley18a}, and there are natural operations computable by
low-order recursion but not by high-order iteration % low-order recursion but not by high-order iteration
\citep{Longley19}. Much of this territory, including the mathematical % \citep{Longley19}. Much of this territory, including the mathematical
theory of some of the natural notions of higher-order computability % theory of some of the natural notions of higher-order computability
that arise in this way, is mapped out by \citet{LongleyN15}. % that arise in this way, is mapped out by \citet{LongleyN15}.
% Relatively few results of this character have so far been established % Relatively few results of this character have so far been established
% on the complexity side. \citet{Pippenger96} gives an example of an % on the complexity side. \citet{Pippenger96} gives an example of an
@@ -14985,18 +14985,18 @@ the other hand, if we extend our language with effect handlers, it
becomes possible to bring the runtime down to $\BigO(2^n)$: an becomes possible to bring the runtime down to $\BigO(2^n)$: an
asymptotic gain of a factor of $n$. asymptotic gain of a factor of $n$.
The \emph{generic search} problem is just like the generic count % The \emph{generic search} problem is just like the generic count
problem, except rather than counting the vectors $q$ such that $P\,q = % problem, except rather than counting the vectors $q$ such that $P\,q =
\True$, it returns the list of all such vectors. % \True$, it returns the list of all such vectors.
% % %
The $\Omega(n 2^n)$ runtime for purely functional implementations % The $\Omega(n 2^n)$ runtime for purely functional implementations
transfers directly to generic search, as generic count reduces to % transfers directly to generic search, as generic count reduces to
generic search composed with computing the length of the resulting % generic search composed with computing the length of the resulting
list. % list.
% % %
In Section~\ref{sec:count-vs-search} we illustrate that the % In Section~\ref{sec:count-vs-search} we illustrate that the
$\BigO(2^n)$ runtime for generic count with effect handlers also % $\BigO(2^n)$ runtime for generic count with effect handlers also
transfers to generic search. % transfers to generic search.
The idea behind the speedup is easily explained and will already be The idea behind the speedup is easily explained and will already be
familiar, at least informally, to programmers who have worked with familiar, at least informally, to programmers who have worked with
@@ -18080,22 +18080,50 @@ However, the effectful implementation runs between 2 and 14 times as
fast with SML/NJ compared with MLton. fast with SML/NJ compared with MLton.
\section{Related work} \section{Related work}
Relatively few results of character of the result in this chapter have There are relatively little work in the present literature on
thus far been established in literature. \citet{Pippenger96} gives an expressivity that has focused on complexity difference.
example of an `online' operation on infinite sequences of atomic %
symbols (essentially a function from streams to streams) such that the \citet{Pippenger96} gives an example of an online operation on
first $n$ output symbols can be produced within time $\BigO(n)$ if one infinite sequences of atomic symbols (essentially a function from
is working in an effectful version of Lisp (one which allows mutation streams to streams) such that the first $n$ output symbols can be
of cons pairs) but with a worst-case runtime no better than produced within time $\BigO(n)$ if one is working in an effectful
$\Omega(n \log n)$ for any implementation in pure Lisp (without such version of Lisp (one which allows mutation of cons pairs) but with a
mutation). This example was reconsidered by \citet{BirdJdM97} who worst-case runtime no better than $\Omega(n \log n)$ for any
showed that the same speedup can be achieved in a pure language by implementation in pure Lisp (without such mutation). This example was
using lazy evaluation. \citet{Jones01} explores the approach of reconsidered by \citet{BirdJdM97} who showed that the same speedup can
manifesting expressivity and efficiency differences between certain be achieved in a pure language by using lazy evaluation.
languages by artificially restricting attention to `cons-free' \citet{Jones01} explores the approach of manifesting expressivity and
programs; in this setting, the classes of representable first-order efficiency differences between certain languages by artificially
functions for the various languages are found to coincide with some restricting attention to `cons-free' programs; in this setting, the
well-known complexity classes. classes of representable first-order functions for the various
languages are found to coincide with some well-known complexity
classes.
The vast majority of work in this area has focused on computability
differences. One of the best known examples is the \emph{parallel if}
operation which is computable in a language with parallel evaluation
but not in a typical sequential programming
language~\cite{Plotkin77}. It is also well known that the presence of
control features or local state enables observational distinctions
that cannot be made in a purely functional setting: for instance,
there are programs involving call/cc that detect the order in which a
(call-by-name) `+' operation evaluates its arguments
\citep{CartwrightF92}. Such operations are `non-functional' in the
sense that their output is not determined solely by the extension of
their input (seen as a mathematical function
$\N_\bot \times \N_\bot \rightarrow \N_\bot$);
%%
however, there are also programs with `functional' behaviour that can
be implemented with control or local state but not without them
\citep{Longley99}. More recent results have exhibited differences
lower down in the language expressivity spectrum: for instance, in a
purely functional setting \textit{\`a la} Haskell, the expressive
power of \emph{recursion} increases strictly with its type level
\citep{Longley18a}, and there are natural operations computable by
low-order recursion but not by high-order iteration
\citep{Longley19}. Much of this territory, including the mathematical
theory of some of the natural notions of higher-order computability
that arise in this way, is mapped out by \citet{LongleyN15}.
\part{Conclusions} \part{Conclusions}
\label{p:conclusions} \label{p:conclusions}