Add arithmetic server example

thesis.tex

@@ -196,9 +196,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
 
 Στο κεφάλαιο 4 παρουσιάζουμε τη θεωρία και την υπάρχουσα δουλειά πίσω από τα συστήματα τύπων συνεδρίας.
 
-Στο κεφάλαιο 5 αναλύουμε το σύστημα που υλοποιήσαμε.
-
-Στο κεφάλαιο 6 παρουσιάζουμε μερικά παραδείγματα χρήσης του συστήματός μας. Τα παραδείγματα αυτά αποτελούνται τόσο από
+Στο κεφάλαιο 5 αναλύουμε το σύστημα που υλοποιήσαμε, και παρουσιάζουμε μερικά παραδείγματα χρήσης του συστήματός μας. Τα παραδείγματα αυτά αποτελούνται τόσο από
 σχετικά απλουστευμένα προγράμματα, τα οποία είναι τυποποιημένα στη σχετική βιβλιογραφία, αλλά και παραδείγματα
 προσαρμοσμένα στο να αναδείξουν τα προτερήματα της υλοποίησής μας.
 
@@ -354,43 +352,65 @@ $otp/lib/compiler/src/core\_parse.hrl$.
     end.
 \end{lstlisting}
 
-% FIXME uppercase greek letters
 \section{Κλασσικά συστήματα τύπων με συμπερασμό}
+Τα πρώτα στατικά συστήματα τύπων βασίζονταν σε type annotations τα οποία παρείχε ο χρήστης. Αυτά ήταν ετικέτες που
+συνόδευαν τις δηλώσεις μεταβλητών και συναρτήσεων, και περιέγραφαν τον τύπο που αυτές θα περιείχαν (στην περίπτωση
+μεταβλητών), ή τους τύπους των ορισμάτων και της τελικής τιμής τους (στην περίπτωση συναρτήσεων), και υπηρετούσαν ως
+οδηγίες προς τον μεταγλωττιστή. Κατά το χρόνο μεταγλώττισης, αυτός ήταν υπεύθυνος να συγκρίνει τον δηλωθέντα τύπο μιας
+μεταβλητής ή συνάρτησης με τους προσδοκόμενους τύπους στο σημείο που αυτά τα constructs χρησιμοποιούνται σε ένα
+πρόγραμμα, προκειμένου να διαπιστώσει αν υπάρχουν ασυμφωνίες τύπων.
+
+Προκειμένου να εξαλειφθεί η ανάγκη για τη χειρονακτική δήλωση των τύπων τμημάτων δεδομένων σε ένα πρόγραμμα,
+αναπτύχθηκαν συστήματα τύπων με αυτόματο συμπερασμό τύπων, όπως αυτό των Hindley-Milner (ή αλλιώς Dammas-Milner), με την
+γλώσσα ML να είναι η πρώτη που υλοποίησε ένα τέτοιο σύστημα.
+
 Η προσέγγιση των συστημάτων τύπων είναι να συσχετίζουν τύπους με προγράμματα. Οι τύποι περιγράφουν το είδος των δεδομένων
 τα οποία μεταχειρίζεται το πρόγραμμα. Ο συσχετισμός αυτός γίνεται μέσω ενός συνόλου κανόνων συμπερασμού, με βάση
 τη σύνταξη του προγράμματος, κάνοντας χρήση ενός περιβάλλοντος τύπων, το οποίο αντιστοιχεί τις ελεύθερες μεταβλητές ενός
-προγράμματος με τους τύπους τους. Η αντιστοίχηση αυτή εκφράζεται με μια σχέση του τύπου $ \Gamma |- e : τ $, όπου:
+προγράμματος με τους τύπους τους. Η αντιστοίχηση αυτή εκφράζεται με μια σχέση του τύπου $ \Gamma |- e : \tau $, όπου:
 \begin{itemize}
     \item $\Gamma$ είναι το περιβάλλον τύπων
     \item $e$ είναι το πρόγραμμα υπό εξέταση
-    \item $τ$ είναι ο τύπος του προγράμματος $e$, δεδομένων των "περιορισμών" που τίθενται σχετικά με τις ελεύθερες
+    \item $\tau$ είναι ο τύπος του προγράμματος $e$, δεδομένων των "περιορισμών" που τίθενται σχετικά με τις ελεύθερες
         μεταβλητές που εμφανίζονται στο σώμα του $e$ από το περιβάλλον $\Gamma$
 \end{itemize}
 
-Οι προκλήσεις του σχεδιασμού ενός συστήματος τύπων είναι:
+Οι προκλήσεις του σχεδιασμού ενός συστήματος συμπερασμού τύπων είναι:
 \begin{itemize}
     \item Το σύστημα τύπων να είναι σημασιολογικά ορθό %% TODO elaborate
     \item Το σύστημα τύπων να είναι αποφάνσιμο, το οποίο σημαίνει ότι πρέπει να είναι δυνατός ο σχεδιασμός ενός
         αλγορίθμου ο οποίος να τερματίζει και να ελέγχει τις ιδιότητες του συστήματος
 \end{itemize}
 
-%% TODO simple type system (look at pl2 slides?)
-
 %FIXME annotations <-> ετικετών
 \section{Συστήματα τύπων με ετικέτες}
 Μια προσέγγιση για την επέκταση της εκφραστικότητας ενός συστήματος τύπων είναι η προσθήκη ετικετών στους τύπους με
-αποτέλεσμα την παραμετροποίησή τους, και στόχο το να καταστεί εφικτό ένα σύνολο στατικών αναλύσεων, όπως η ανάλυση ροής
-ελέγχου σε έναν μεταγλωττιστή.
-
-%% TODO simple annotated type system
+αποτέλεσμα την παραμετροποίησή τους. Στόχος αυτής της επέκτασης είναι το να καταστεί εφικτό ένα σύνολο στατικών αναλύσεων,
+όπως:
+\begin{itemize}
+        % FIXME bind-time <-> χρονος δεσίματος
+    \item Ανάλυση χρόνου δεσίματος, κατα την οποία προσπαθούμε να πραγματοποιήσουμε μια διάκριση ανάμεσα σε αυτά δεδομένα των
+        οποίων η τιμή είναι γνωστή κατα το χρόνο μεταγλώττισης (στατικά), και σε αυτά τα οποία αποκτούν τιμή κατα την
+        εκτέλεση του προγράμματος (δυναμικά). Αυτού του τύπου η ανάλυση αποτελεί τη βάση της μερικής αποτίμησης που
+        πραγματοποιούν μεταγλωττιστές
+    \item Ανάλυση χρήσεων, κατά την οποία θέλουμε να μάθουμε πόσες φορές χρησιμοποιείται η τιμή μιας έκφρασης στη
+        διάρκεια της εκτέλεσης ενός προγράμματος. Αν αποφανθούμε ότι δε γίνεται ποτέ χρήση μιας τιμής, ο μεταγλωττιστής
+        δε χρειάζεται να παράξει κώδικα για αυτήν. Επίσης, αν μια τιμή χρησιμοποιείται μόνο μια φορά, η μεταβλητή που
+        την περιέχει μπορεί να συλλεγεί από τον συλλέκτη σκουπιδιών του περιβάλλοντος εκτέλεσης αμέσως μετά τη χρήση
+        της.
+    \item Ανάλυση ροής ελέγχου, κατά την οποία προσπαθούμε, συνήθως σε γλώσσες με συναρτήσης υψηλότερης τάξης, να
+        συμπεράνουμε ποιες συναρτήσεις είναι πιθανοί "αποδέκτες" μιας κλήσης σε ένα πρόγραμμα, δηλαδή ποιες συναρτήσεις
+        είναι πιθανό να αποκτήσουν τον ελέγχο ενός προγράμματος (το οποίο δεν είναι πάντα εμφανές σε γλώσσες τέτοιου
+        τύπου από τον πηγαίο κώδικά τους).
+\end{itemize}
 
 \section{Συστήματα τύπων και επιδράσεων}
 Ο στόχος της προσθήκης πληροφορίας επιδράσεων στα κλασσικά συστήματα τύπων είναι η επέκτασή τους ώστε να εκφράζουν
 επιπλέον ιδιότητες που προκύπτουν από τους σημασιολογικούς κανόνες ενός προγράμματος.
 
-Τα συστήματα τύπων και επιδράσεων αποτελούν ουσιαστικά μια παραλλαγή των annotated συστημάτων τύπων, με μια διαφορά: οι
-ετικέτες σε αυτά εκφράζουν ιδιότητες που αφορούν τη δυναμική συμπεριφορά του προγράμματος, δηλαδή τη συμπεριφορά του
-κατά το χρόνο εκτέλεσης του προγράμματος.
+Τα συστήματα τύπων και επιδράσεων αποτελούν ουσιαστικά μια παραλλαγή των συστημάτων τύπων με ετικέτες στα οποία
+αναφερθήκαμε παραπάνω, αλλά με μια διαφορά: οι ετικέτες σε αυτά τα συστήματα τύπων περιέχουν πληροφορία σχετικά με την
+συμπεριφορά του προγράμματος κατά τον χρόνο αποτίμησης και εκτέλεσής του.
 
 Σε ένα σύστημα τύπων και επιδράσεων, η αντιστοίχιση ενός προγράμματος με έναν τύπο και μια επίδραση γράφεται ως $ \Gamma |- e
 : \tau; \phi $, που σημαίνει ότι στο περιβάλλον $\Gamma$, το πρόγραμμα $e$ εμφανίζει μια επίδραση $\phi$, και εν τέλει επιστρέφει μια
@@ -1056,9 +1076,285 @@ $f/a[v]$.
 θεωρούμε έως και $ \mychoose{n}{2} $ ζευγάρια. Κάτι τέτοιο, αν και αργό, ίσως να είναι εφικτό μόνο για μικρές τιμές του $n$,
 και για σχετικά σύντομους και απλούς τύπους συνεδριών.
 
-% Examples
-\chapter{Παραδείγματα}
-Παρουσίαση των toy παραδειγμάτων με τα οποία δουλεύουμε, και ίσως κάτι πιο involved?
+\section{Παράδειγμα υλοποίσης: Arithmetic Server}
+
+Στην παρούσα ενότητα, παρουσιάζουμε ένα κλασσικό παράδειγμα στην ανάλυση συστημάτων τύπων συνεδριών. Το παράδειγμα αυτό
+αποτελεί μια υλοποίηση του αναδρομικού arithmetic server που πρωτοπεριγράφηκε στο [], με μια διαφορά: έχουμε εξαλείψει
+την έννοια του "καναλιού" μέσω του οποίου ένας client αποστέλει στον διακομιστή το αίτημά του, και το οποίο
+δημιουργείται κατά το αίτημα.
+
+Το πρόγραμμα που υλοποιεί τον arithmetic server, καθώς και clients που αιτούνται πράξεις από αυτόν, έχει ως εξής:
+
+\begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\tiny]
+run() ->
+    Server = spawn(fun server/0),
+    process_flag(trap_exit, true),
+    spawn_link(fun() -> sum_client(Server, rand:uniform(10)) end),
+    spawn_link(fun() -> neg_client(Server, rand:uniform(10)) end),
+    spawn_link(fun() -> sqrt_client(Server, rand:uniform(10)) end),
+    await_termination(Server, 3).
+
+await_termination(Server, 0) -> Server ! {quit, self()}, ok;
+await_termination(Server, N) ->
+    receive
+        {'EXIT', _, _} -> await_termination(Server, N - 1)
+    end.
+
+server() ->
+    receive
+        {sum, Pid} ->
+            receive
+                {sum_o1, Pid, Opand1} ->
+                    receive
+                        {sum_o2, Pid, Opand2} ->
+                            Pid ! {res, self(), Opand1 + Opand2},
+                            server()
+                    end
+            end;
+        {neg, Pid} ->
+            receive
+                {neg_o, Pid, Opand} ->
+                    Pid ! {res, self(), - Opand},
+                    server()
+            end;
+        {sqrt, Pid} ->
+            receive
+                {sqrt_o, Pid, Opand} ->
+                    Pid ! {res, self(), math:sqrt(Opand)},
+                    server()
+            end;
+        {quit, _} ->
+            exit(normal)
+    end.
+
+-spec sum_client(pid(), non_neg_integer()) -> ok.
+sum_client(_Server, 0) -> ok;
+sum_client(Server, N) ->
+    Op1 = rand:uniform(1000),
+    Op2 = rand:uniform(1000),
+    Server ! {sum, self()},
+    Server ! {sum_o1, self(), Op1},
+    Server ! {sum_o2, self(), Op2},
+    receive
+        {res, Server, _Res} ->
+            io:format("sum_client: Sent ~p and ~p, received ~p\n", [Op1, Op2, _Res]),
+            sum_client(Server, N - 1)
+    end.
+
+-spec neg_client(pid(), non_neg_integer()) -> ok.
+neg_client(_Server, 0) -> ok;
+neg_client(Server, N) ->
+    Op = rand:uniform(1000),
+    Server ! {neg, self()},
+    Server ! {neg_o, self(), Op},
+    receive
+        {res, Server, Res} ->
+            io:format("neg_client: Sent ~p, received ~p\n", [Op, Res]),
+            neg_client(Server, N - 1)
+    end.
+
+sqrt_client(_Server, 0) -> ok;
+sqrt_client(Server, N) ->
+    Op = rand:uniform(1000),
+    Server ! {sqrt, self()},
+    Server ! {sqrt_o, self(), Op},
+    receive
+        {res, Server, _Res} ->
+            io:format("sqrt_client: Sent ~p, received ~p\n", [Op, _Res]),
+            sqrt_client(Server, N - 1)
+    end.
+\end{lstlisting}
+
+Και ακολουθούν τα annotations προς το σύστημά μας, που περιγράφουν το πρωτόκολλο που πρέπει να ακολουθείτα από την
+υλοποίησή μας.
+
+\begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\tiny]
+-sestype({{server, 0},
+         ?f_rec_tag(1, [?sa_offer_tag([{?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
+                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
+                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
+                                                       ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_rec_tag(1)]},
+                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
+                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
+                                                       ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_rec_tag(1)]},
+                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
+                                                       ?sa_recv_tag(?dt_integer_tag, ?dt_tuple_tag([])),
+                                                       ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_rec_tag(1)]},
+                                       {?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([]))]}])])}).
+
+-sestype({{sum_client, 2},
+         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_send_tag(1, ?dt_tuple_tag([])),
+                        ?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])),
+                        ?sa_rec_tag(1)])}).
+
+-sestype({{neg_client, 2},
+         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_send_tag(1, ?dt_tuple_tag([])),
+                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])), ?sa_rec_tag(1)])}).
+
+-sestype({{sqrt_client, 2},
+         ?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([])), ?sa_send_tag(1, ?dt_tuple_tag([])),
+                        ?sa_recv_tag(?dt_atom_tag, ?dt_tuple_tag([])), ?sa_rec_tag(1)])}).
+\end{lstlisting}
+
+Τα contracts αυτά μας λένε το εξής:
+\begin{itemize}
+    \item Η συνάρτηση $server/0$ αρχικά περιμένει να λάβει μια τούπλα, η οποία αποτελείται από ένα atom (το οποίο, όπως
+        φαίνεται από τον κώδικα, περιγράφει την αριθμητική πράξη που ο client θέλει να εκτελεστεί εκ μέρους του από τον
+        server), και ένα $pid$, το οποίο αντιστοιχεί στο process του client. Το επόμενο βήμα, ασχέτως με τα περιεχόμενα
+        της τούπλας που θα λάβει, θα είναι να περιμένει και πάλι να λάβει μια τούπλα, η οποία αποτελείται από ένα $atom$,
+        το $pid$ που έλαβε και στο προηγούμενο μήνυμα, και έναν αριθμό, στις δύο περιπτώσεις ακεραίου τύπου. Το επόμενο
+        βήμα εξαρτάται από το path που έχουμε διανύσει ως τώρα:
+        \begin{itemize}
+            \item Υπάρχει περίπτωση ο client να αιτείτα πράξη αντιστροφής προσήμου, οπότε εδώ ο server θα αποστείλει μια
+                απάντηση στο $pid$ του client, η οποία αποτελείται από μια τουπλα που περιέχει ένα $atom$, το $pid$ του
+                server, και το αποτέλεσμα της πράξης
+            \item Αν από την άλλη ο client αιτείται εκτέλεση πράξης εύρεσης τετραγωνικής ρίζας, τότε ο server και πάλι
+                θα αποστείλει μια τούπλα στον client, ίδιου τύπου με αυτήν της προηγούμενης περίπτωσης.
+            \item Σε περίπτωση που το αίτημα είναι για άθροιση αριθμών, τότε ο server θα περιμένει ένα ακόμη μήνυμα απο
+                τον client, με τον δεύτερο τελεσταίο της πράξης. Μόλις λάβει και αυτόν, θα επιστρέψει μια τούπλα
+                αντίστοιχη με τις προηγούμενες δύο.
+        \end{itemize}
+        Και στις τρεις περιπτώσεις, η εκτέλεση του server συνεχίζεται με την αναδρομική κλήση της $server/0$.
+    \item Η συνάρτηση $sum\_client/2$ υλοποιεί έναν client ο οποίος αιτείται μόνο πράξεις άθροισης από τον server.
+        Στέλνει τρία μηνύματα στη σειρά, εκ των οποίων το πρώτο περιέχει ένα $atom sum$ και το $pid$ του, και τα επόμενα
+        δύο περιέχουν ένα $atom$, το $pid$ του και από έναν ακέραιο, και περιμένει να λάβει πίσω μια τούπλα που
+        περιέχει ένα $atom$, στην προκειμένη το $res$, το $pid$ του server, και το αποτέλεσμα της πράξης που
+        αιτήθηκε. Ακολούθως, καλείται αναδρομικά η $sum\_client/2$.
+    \item Η συνάρτηση $neg\_client/2$ υλοποιεί έναν client που αιτείται συνεχώς πράξεις αντιστροφής προσήμου από τον
+        server. Αποστέλει στην αρχή ένα μήνυμα που περιέχει το $atom neg$, ακολουθούμενο από το $pid$ του negation
+        client, και στη συνέχεια αποστέλει μια τούπλα που περιέχει ένα $atom$, το $pid$ του, και τον αριθμό που θα
+        τελέσει χρέη τελεσταίου. Ακολούθως, περιμένει απάντηση με ένα $atom$ (το $res$), το $pid$ του server, και το
+        αποτέλεσμα της πράξης, πρωτού καλέσει αναδρομικά τον εαυτό της.
+    \item Η συνάρτηση $sqrt\_client/2$ συμπεριφέρεται με ακριβώς τον ίδιο τρόπο όπως η $neg\_client/2$, με τη διαφορά
+        ότι αποστέλει ένα $atom sqrt$ αντί για $neg$ στο πρώτο της μήνυμα.
+\end{itemize}
+
+Στα σχήματα 6.1 έως 6.4 φαίνονται οι τύποι συνεδρίας των παραπάνω συναρτήσεων, σε μορφή γραφήματος.
+
+\begin{figure}[ht]
+    \caption{server/0}
+    \centering
+    \includegraphics[scale=0.4]{arithmetic/server_0.png}
+\end{figure}
+
+\begin{figure}[ht]
+    \caption{sum\_client/2}
+    \centering
+    \includegraphics[scale=0.5]{arithmetic/sum_client_2.png}
+\end{figure}
+
+\begin{figure}[ht]
+    \caption{neg\_client/2}
+    \centering
+    \includegraphics[scale=0.5]{arithmetic/neg_client_2.png}
+\end{figure}
+
+\begin{figure}[ht]
+    \caption{sqrt\_client/2}
+    \centering
+    \includegraphics[scale=0.5]{arithmetic/sqrt_client_2.png}
+\end{figure}
+
+
+Αναλύοντας την υλοποίηση αυτή με το σύστημά μας, παίρνουμε αρχικά τους συμπερασμένους τύπους διεργασιών των συναρτήσεων
+που αποτελούν το πρόγραμμα:
+
+\begin{lstlisting}[language=Erlang, caption=Inferred Session Types of Arithmetic Server, basicstyle=\tiny]
+{server,0} : "u (4). Of<any; ?(atom x {atom, pid, (atom x atom)}).
+                             ?(atom x {atom, pid, (atom x atom)} x number).
+                             ?(atom x {atom, pid, (atom x atom)} x number).
+                             pid(1) !(atom x pid x number).rec(4).,any;
+                             ?(atom x {atom, pid, (atom x atom)}).
+                             ?(atom x {atom, pid, (atom x atom)} x number).
+                             pid(1) !(atom x pid x number).rec(4).,any;
+                             ?(atom x {atom, pid, (atom x atom)}).
+                             ?(atom x {atom, pid, (atom x atom)} x number).
+                             pid(1) !(atom x pid x float).rec(4).,any;
+                             ?(atom x any).>."
+
+{sum_client,2} : "u (3). pid(1) !(atom x pid).
+                         pid(1) !(atom x pid x integer).
+                         pid(1) !(atom x pid x integer).
+                         ?(atom x pid x any).rec(3)."
+
+{neg_client,2} : "u (2). pid(1) !(atom x pid).
+                         pid(1) !(atom x pid x integer).
+                         ?(atom x pid x any).rec(2)."
+
+{sqrt_client,2} : "u (1). pid(1) !(atom x pid).
+                          pid(1) !(atom x pid x integer).
+                          ?(atom x pid x any).rec(1)."
+\end{lstlisting}
+
+Καθώς δεν εμφανίστηκε κάποιο σφάλμα κατά τη σύγκριση των τύπων που το σύστημά μας συμπέρανε για τις υλοποιηθείσες
+συναρτήσεις με τους τύπους που παρείχε ο χρήστης μέσω των $-sestype()$ annotations, διαπιστώνουμε ότι οι συναρτήσεις
+πράγματι υλοποιούν το επιθυμητό πρωτόκολλο.
+
+Ακολούθως, προσπαθούμε να δούμε αν όντως μπορεί να διαδραματιστεί επιτυχής επικοινωνία ανάμεσα στα endpoints μας.
+Αρχικά, έχουμε τον server με τον client άθροισης, $sum\_client/2$.
+
+\begin{lstlisting}[language=Erlang, caption=server/0 and sum\_client/2, basicstyle=\tiny]
+{server,0} and {sum_client,2} are peers
+The matching sequences are:
+[{{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]}]}},
+  {send,{other_proc,1},{tuple,[atom,pid]}}},
+ {{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]},number]}},
+  {send,{other_proc,1},{tuple,[atom,pid,integer]}}},
+ {{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]},number]}},
+  {send,{other_proc,1},{tuple,[atom,pid,integer]}}},
+ {{send,{other_proc,1},{tuple,[atom,pid,number]}},
+  {recv,any,{tuple,[atom,pid,any]}}}]
+\end{lstlisting}
+
+Όπως θα έπρεπε, το σύστημά μας βρίσκει ένα παράδειγμα επιτυχούς επικοινωνίας μεταξύ των δύο συναρτήσεων, παρουσιάζοντάς
+μας τα ζευγάρια των δυικών πράξεων επικοινωνίας.
+
+Τα πράγματα για τους $neg\_client/2$ και $sqrt\_client/2$ είναι ελαφρώς διαφορετικά:
+
+\begin{lstlisting}[language=Erlang, caption=neg\_client/2 and sqrt\_client/2, basicstyle=\tiny]
+
+{server,0} and {neg_client,2} are peers
+The matching sequences are:
+[{{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]}]}},
+  {send,{other_proc,1},{tuple,[atom,pid]}}},
+ {{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]},number]}},
+  {send,{other_proc,1},{tuple,[atom,pid,integer]}}},
+ {{send,{other_proc,1},{tuple,[atom,pid,float]}},
+  {recv,any,{tuple,[atom,pid,any]}}}]
+[{{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]}]}},
+  {send,{other_proc,1},{tuple,[atom,pid]}}},
+ {{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]},number]}},
+  {send,{other_proc,1},{tuple,[atom,pid,integer]}}},
+ {{send,{other_proc,1},{tuple,[atom,pid,number]}},
+  {recv,any,{tuple,[atom,pid,any]}}}]
+
+{server,0} and {sqrt_client,2} are peers
+The matching sequences are:
+[{{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]}]}},
+  {send,{other_proc,1},{tuple,[atom,pid]}}},
+ {{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]},number]}},
+  {send,{other_proc,1},{tuple,[atom,pid,integer]}}},
+ {{send,{other_proc,1},{tuple,[atom,pid,float]}},
+  {recv,any,{tuple,[atom,pid,any]}}}]
+[{{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]}]}},
+  {send,{other_proc,1},{tuple,[atom,pid]}}},
+ {{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]},number]}},
+  {send,{other_proc,1},{tuple,[atom,pid,integer]}}},
+ {{send,{other_proc,1},{tuple,[atom,pid,number]}},
+  {recv,any,{tuple,[atom,pid,any]}}}]
+
+\end{lstlisting}
+
+Παρόλο που (σωστά) το σύστημά μας αποφαίνεται ότι τα ζευγάρια των δύο clients με τον server είναι πράγματι εταίροι
+επικοινωνίας, εσφαλμένα υπολογίζει δύο εναλλακτικά επιτυχή "σενάρια" επικοινωνίας για κάθε έναν από τους δύο clients.
+Αυτό οφείλεται στο γεγονός ότι κατά την ανάλυση λαμβάνουμε υπόψιν μας μόνο τους τύπους των στοιχείων δεδομένων, και όχι
+τις τιμές τους. Καθώς τα μονοπάτια επικοινωνίας για τις περιπτώσεις της αντιστροφής προσήμου και του υπολογισμού
+τετραγωνικής ρίζας είναι ίδια τόσο ως προς τα βήματα, όσο και στους τύπους δεδομένων των μηνυμάτων που ανταλλάσσονται
+ανάμεσα στους clients και τον server, το σύστημά μας τα θεωρεί έγκυρα, ενώ στην πραγματικότητα, μόνο το ένα από τα δύο
+είναι έγκυρο για κάθε client.
+
+Μια πιθανή λύση γι'αυτό το πρόβλημα θα μπορούσε να είναι το να θεωρούσαμε το κάθε literal atom
+στον κώδικα των προγραμμάτων που αναλύουμε σαν ένα singleton type, κατα παρόμοιο τρόπο όπως αντιμετωπίζουμε τα pids.
 
 \chapter{Συμπεράσματα και μελλοντική έρευνα}
 
@@ -1068,14 +1364,16 @@ $f/a[v]$.
 % TODO maybe here we also need to talk about conclusions we have come to about the pros/cons of our technique, especially when compared
 % to the various monitoring techniques we talk about [i.e static vs dynamic session type systems].
 
-Κατά τη χρήση του εν λόγω συστήματος, διαπιστώσαμε ότι υπάρχει ένα σύνολο προσθηκών και αλλαγών που θα έπρεπε να γίνουν
+Κατά την ανάπτυξη και χρήση του εν λόγω συστήματος, διαπιστώσαμε ότι υπάρχει ένα σύνολο προσθηκών και αλλαγών που θα έπρεπε να γίνουν
 σε αυτό, προκειμένου να μπορεί να χρησιμοποιηθεί αποτελεσματικά για την ανάλυση υπάρχουσων βάσεων κώδικα, αλλά και
 ως ένα βοηθητικό εργαλείο αποσφαλμάτωσης κατά τη φάση της ανάπτυξης νέων εφαρμογών.
+
+Συγκεκριμένα:
 \begin{itemize}
     \item Το παρόν σύστημα τύπων μας δεν είναι σε θέση να μοντελοποιήσει αμιγώς αναδρομικές συναρτήσεις.
     \item Τα session type annotations που μπορεί να εισάγει κανείς στα modules θα έπρεπε να παρέχονται με έναν τρόπο πιο φιλικό
-        προς τον χρήστη, όπως μια συμβολοσειρά που μοιάζει περισσότερο με την περιγραφή των session types όπως τη
-        συναντάει κανείς στη βιβλιογραφία.
+        προς τον χρήστη, όπως, για παράδειγμα, σαν μια συμβολοσειρά που μοιάζει περισσότερο με την περιγραφή των session types
+        με τον τρόπο που αυτή συναντάται στη βιβλιογραφία.
         % TODO an example here would be nice.
     \item Ο μηχανισμός επαλήθευσης των peer session types επιδέχεται σοβαρών βελτιστοποιήσεων, κυρίως σε περιπτώσεις
         όπου αντιμετωπίζουμε αναδρομικούς τύπους.
@@ -1086,7 +1384,7 @@ $f/a[v]$.
         σε ένα τέτοιο search space. Η εισαγωγή τεχνικών που έχουν χρησιμοποιηθεί με επιτυχία στην περίπτωση του stateless
         model checking [], καθώς επίσης και η εφαρμογή μεθόδων επέκτασης κατευθυνόμενων κυκλικών γραφημάτων μπορεί να
         αποδειχθούν ιδιαίτερα αποτελεσματικές για την επίτευξη αυτού του στόχου.
-    \item Ο μηχανισμός συμπερασμού τύπων δεδομένων εξακολουθεί να είναι suboptimal, όμως δεν είναι ξεκάθαρο το πώς θα
+    \item Ο μηχανισμός συμπερασμού τύπων δεδομένων απέχει από το να είναι ο βέλτιστος δυνατός, όμως δεν είναι ξεκάθαρο το πώς θα
         μπορούσε να βελτιωθεί, δεδομένων των περιορισμών των γλωσσών προγραμματισμού με δυναμικά συστήματα τύπων.
     \item Η επέκταση του συστήματος ώστε να είναι σε θέση να διαχειριστεί και τύπους δεδομένων ορισμένους από τον χρήστη.
 \end{itemize}