From adb9a987b33a7bc73a67e37a932448c79cc26085 Mon Sep 17 00:00:00 2001 From: Thomas Pietrzak Date: Mon, 28 Mar 2022 18:12:59 +0200 Subject: [PATCH] A bit of machine behavior --- mystyle.sty | 135 ++++++++++++++++++++++++++++++++++++++++++++++++- tex/4-loop.tex | 116 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 249 insertions(+), 2 deletions(-) diff --git a/mystyle.sty b/mystyle.sty index f8c12bd..3c3477d 100644 --- a/mystyle.sty +++ b/mystyle.sty @@ -407,7 +407,9 @@ \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}} @@ -571,6 +573,7 @@ % 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 @@ -627,4 +630,132 @@ \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 +} diff --git a/tex/4-loop.tex b/tex/4-loop.tex index 23f5192..25c4d88 100644 --- a/tex/4-loop.tex +++ b/tex/4-loop.tex @@ -436,6 +436,122 @@ In my opinion thus is a limitation for the generative aspect of these models, an \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} -- 2.30.2