\newcommand{\etal}{\emph{et al.}\xspace}
-\newcommand{\fixme}[1]{\color{red}#1\color{black}\xspace}
+\newcommand{\fixme}[1]{\textcolor{red}{#1}\xspace}
+
+\newcommand{\todo}[1]{\textcolor{blue}{[#1]}\xspace}
\makeatletter
\newcommand{\centrevertical}[1]{\raisebox{-\height + \ht\@arstrutbox}{#1}}
% Change volume.number format to volume(number)
\renewbibmacro*{volume+number+eid}{%
+ \setunit{\addcomma\space}%
\printfield{volume}%
% \setunit*{\adddot}% DELETED
% \setunit*{\addnbspace}% NEW (optional); there's also \addnbthinspace
\renewcommand*{\mkbibnamefamily}[1]{%
\ifitemannotation{highlight}
{\textbf{#1}}
- {#1}}
\ No newline at end of file
+ {#1}}
+
+% For code listings
+\usepackage{listings}
+
+\lstset{numbers=left, tabsize=2, frame=single, float=htb}
+
+\lstnewenvironment{code}[1][]%
+ {\noindent\minipage{\linewidth}\medskip
+ \lstset{basicstyle=\ttfamily\footnotesize,lineskip=2pt,frame=tb,#1}}
+ {\endminipage}
+
+% Coq listings
+\definecolor{dkgreen}{rgb}{0,0.6,0}
+\definecolor{ltblue}{rgb}{0,0.4,0.4}
+\definecolor{dkviolet}{rgb}{0.3,0,0.5}
+
+% lstlisting coq style (inspired from a file of Assia Mahboubi)
+\lstdefinelanguage{Coq}{
+ % Anything betweeen $ becomes LaTeX math mode
+ mathescape=true,
+ % Comments may or not include Latex commands
+ texcl=false,
+ % Vernacular commands
+ morekeywords=[1]{Section, Module, End, Require, Import, Export,
+ Variable, Variables, Parameter, Parameters, Axiom, Hypothesis,
+ Hypotheses, Notation, Local, Tactic, Reserved, Scope, Open, Close,
+ Bind, Delimit, Definition, Let, Ltac, Fixpoint, CoFixpoint, Add,
+ Morphism, Relation, Implicit, Arguments, Unset, Contextual,
+ Strict, Prenex, Implicits, Inductive, CoInductive, Record,
+ Structure, Canonical, Coercion, Context, Class, Global, Instance,
+ Program, Infix, Theorem, Lemma, Corollary, Proposition, Fact,
+ Remark, Example, Proof, Goal, Save, Qed, Defined, Hint, Resolve,
+ Rewrite, View, Search, Show, Print, Printing, All, Eval, Check,
+ Projections, inside, outside, Def},
+ % Gallina
+ morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
+ match, with, end, as, in, return, let, if, is, then, else, for, of,
+ nosimpl, when},
+ % Sorts
+ morekeywords=[3]{Type, Prop, Set, true, false, option},
+ % Various tactics, some are std Coq subsumed by ssr, for the manual purpose
+ morekeywords=[4]{pose, set, move, case, elim, apply, clear, hnf,
+ intro, intros, generalize, rename, pattern, after, destruct,
+ induction, using, refine, inversion, injection, rewrite, congr,
+ unlock, compute, ring, field, fourier, replace, fold, unfold,
+ change, cutrewrite, simpl, have, suff, wlog, suffices, without,
+ loss, nat_norm, assert, cut, trivial, revert, bool_congr, nat_congr,
+ symmetry, transitivity, auto, split, left, right, autorewrite},
+ % Terminators
+ morekeywords=[5]{by, done, exact, reflexivity, tauto, romega, omega,
+ assumption, solve, contradiction, discriminate},
+ % Control
+ morekeywords=[6]{do, last, first, try, idtac, repeat},
+ % Comments delimiters, we do turn this off for the manual
+ morecomment=[s]{(*}{*)},
+ % Spaces are not displayed as a special character
+ showstringspaces=false,
+ % String delimiters
+ morestring=[b]",
+ morestring=[d],
+ % Size of tabulations
+ tabsize=3,
+ % Enables ASCII chars 128 to 255
+ extendedchars=false,
+ % Case sensitivity
+ sensitive=true,
+ % Automatic breaking of long lines
+ breaklines=false,
+ % Default style fors listings
+ basicstyle=\small,
+ % Position of captions is bottom
+ captionpos=b,
+ % flexible columns
+ columns=[l]flexible,
+ % Style for (listings') identifiers
+ identifierstyle={\ttfamily\color{black}},
+ % Style for declaration keywords
+ keywordstyle=[1]{\ttfamily\color{dkviolet}},
+ % Style for gallina keywords
+ keywordstyle=[2]{\ttfamily\color{dkgreen}},
+ % Style for sorts keywords
+ keywordstyle=[3]{\ttfamily\color{ltblue}},
+ % Style for tactics keywords
+ keywordstyle=[4]{\ttfamily\color{dkblue}},
+ % Style for terminators keywords
+ keywordstyle=[5]{\ttfamily\color{dkred}},
+ %Style for iterators
+ %keywordstyle=[6]{\ttfamily\color{dkpink}},
+ % Style for strings
+ stringstyle=\ttfamily,
+ % Style for comments
+ commentstyle={\ttfamily\color{dkgreen}},
+ %moredelim=**[is][\ttfamily\color{red}]{/&}{&/},
+ literate=
+ {\\forall}{{\color{dkgreen}{$\forall\;$}}}1
+ {\\exists}{{$\exists\;$}}1
+ {<-}{{$\leftarrow\;$}}1
+ {=>}{{$\Rightarrow\;$}}1
+ {==}{{\code{==}\;}}1
+ {==>}{{\code{==>}\;}}1
+ % {:>}{{\code{:>}\;}}1
+ {->}{{$\rightarrow\;$}}1
+ {<->}{{$\leftrightarrow\;$}}1
+ {<==}{{$\leq\;$}}1
+ {\#}{{$^\star$}}1
+ {\\o}{{$\circ\;$}}1
+ {\@}{{$\cdot$}}1
+ {\/\\}{{$\wedge\;$}}1
+ {\\\/}{{$\vee\;$}}1
+ {++}{{\code{++}}}1
+ {~}{{\ }}1
+ {\@\@}{{$@$}}1
+ {\\mapsto}{{$\mapsto\;$}}1
+ {\\hline}{{\rule{\linewidth}{0.5pt}}}1
+ %
+}[keywords,comments,strings]
+
+\usepackage{caption}
+
+\DeclareCaptionFormat{listing} {%
+ \textbf{#1#2}#3
+}
+\DeclareCaptionLabelSeparator{listing}{~--~}
+\captionsetup[lstlisting]{format=listing, %
+ labelsep=listing, %
+ justification=raggedright, %
+ singlelinecheck=off
+}
\subsection{System architectures and paradigms}
+The overall behavior of machines is similar to human behavior: they take inputs, process them and produce an output.
+%However the way they behave this way and most importantly the purpose of their behavior is different.
+However, the way this process runs is different.
+
+\paragraph{Computation}
+
+Computers and programs are based on theoretical models such as $\lambda$-calculus~\cite{church32} or Turing machines~\cite{turing38}.
+These are computing models, and they focus on solving numerical problem.
+A Turing machine has an infinite tape with symbols written in advance, and a pre-defined transition table that describes the behavior of the machine.
+Therefore these machines ignore their environment, in which anything can change at anytime.
+All these models are equivalent (or Turing-equivalent), and the Church-Turing thesis says that everything these models can compute can be implemented with an algorithm.
+Wegner and Goldin explain that both this universality and this limitation are due to their inductive nature~\cite{wegner99}.
+
+Induction require structures to be finite, and computation to end.
+For example the Listing~\ref{lst:induction} shows the inductive definition of a list of numbers, and a function that computes the length of a list.
+A list is buit with two constructors: either a \verb+Nil+ value for an empty list, or a \verb+Cons+ function that create a list with a number (the head) and another list (the tail).
+The \verb+Nil+ value ensures that the list is finite.
+It ensures in turn that the \verb+length+ function ends, because there is no recursive call on the base case (\verb+Nil+).
+
+\begin{code}[language=Coq, label=lst:induction, caption=Inductive list and example of inductive function on a list.]
+ Inductive list : Set :=
+ | Nil : list
+ | Cons : nat -> list -> list.
+
+ Fixpoint length (l: list) : nat :=
+ match l with
+ | Nil => 0
+ | Cons _ s' => 1 + (length s')
+ end.
+\end{code}
+
+This simple example shows the rigidity of algorithmic behavior.
+All information about the problem must be known in advance, the computing process is precisely defined, and the output is specified by the inputs~\cite{knuth68}.
+Wegner and Goldin describe interaction as a more general model in which the machine is connected to input streams, that provide unpredictable data~\cite{goldin08}.
+They model interaction with co-induction as in the example in Listing~\ref{lst:coinduction}.
+This example defines a stream of numbers, which is an non-finite structure, and a function that returns another stream in which numbers from the input stream are multplied by $2$.
+The co-inductive definition of the stream only has one constructor, identical to the second constructor of lists.
+The absence of a base constructor make streams infinite structures.
+Therefore recursive function on streams potentially run forever.
+Hence, there is no equivalent of a \verb+length+ function because it would never return a value.
+However, functions such as in this example make sense.
+
+\begin{code}[language=Coq, label=lst:coinduction, caption=Co-inductive stream and example of co-inductive function on a stream.]
+ CoInductive stream : Set :=
+ Cons : nat -> stream -> stream.
+
+ CoFixpoint double (s: stream) : stream :=
+ match s with
+ | Cons x s' => Cons (2 * x) (double s')
+ end.
+\end{code}
+
+We observe here that each iteration of the co-fixpoint can be inductive, as it is the case in the example.
+It shows that interaction is a general process that connects entities in the environment to enable them exchanging information.
+Algorithms only process information to transform input into outputs without knowledge of the overall scheme.
+\todo{Maybe move stuff below to the discussion…}
+Wegner describe several kinds of what he calls \defwords{interaction machines}{interaction machine}.
+He gives the a machine that simply echoes an input stream to an output stream~\cite{wegner97} to demonstrate the power of the interaction phenomenon.
+Such a basic machine connected to two humans can pass the Turing test without being particularly intelligent.
+It can win half of chess games between these two people.
+When I discussed this with \fixme{Gérard Berry}, he said this was cheating.
+\todo{Should I remove the name?}
+But it is no different from AlphaZero which processes human knowledge to beat chess world champions~\cite{silver18}.
+Further, Algorithms are immutable human behavior and knowledge.
+%In fact in this latter case we often cite it as a superiority of machines.
+When the machine wins the game the reward is for the machine designer not for the machine.
+
+
+% \begin{algorithm}[htb]
+% \SetAlgoLined
+% \caption{Typical main function of an interactive application}
+% \While{true}{
+% get inputs\;
+% update internal model\;
+% generate outputs\;
+% }
+% \end{algorithm}
+
+
+
+
+
+%, and overlook the interaction machines have with their environment.
+% While people daily interact with a world full of interactive devices, machines constantly interact with the world full of humans.
+% Because of that, Goldin and Wegner showed that interaction is a more general model of computing that Turing-complete models~\cite{goldin08}.
+% They argue that the universality of the computing models above is due to the fact they all rely on induction~\cite{wegner99}.
+% Interaction is rather a co-inductive phenomenon.
+
+
+
+
+
+% The induction mechanism converges to base cases, which ensures computation always terminates.
+% At the opposite, co-induction is a process that applies to streams as input are received.
+% The question whether the co-inductive process terminates is not relevant.
+% It potentially runs forever on an infinite input stream.
+% This is a necessary mechanism to model and implement interaction with external agents.
+
+Pb: it reacts always the same way to the same entries. Humans tend to evolve. => ML?
+Flexibility? Adaptability?
+
+
+PAC \cite{coutaz87}
+Arch \cite{arch92}
+MVC \cite{reenskaug79a}
+Seeheim \cite{green85}
+
+Différent ? Ou pas ?
+(Not only machines behavior is behavior is different than human behavior), but most importantly the purpose of their behavior is different.
+
+Computers are human inventions, and they are build to follow human-made specifications.
+Their behavior
+
+
+
+
Curiosity~\cite{laversannefinot18}
Arch~\cite{arch92}, MVC~\cite{reenskaug79,reenskaug79a}, PAC~\cite{coutaz87}
projects / hdr.git / commitdiff