# Synthèse de cours : TAS
###### tags: `TAS` `synthèse`

[TOC]

## Lambda calcul
### Expressions

$$
E := E \;\text{(Var)}\;|\; \lambda x.E\;\text{(Abs)} \;|\; E1\;E2\;\text{(App)}
$$

### Beta-reduction ($\rightarrow_\beta$)
Une manière de voir les termes du lambda-calcul consiste à les concevoir comme des arbres ayant des nœuds binaires (les applications), des nœuds unaires (les λ-abstractions) et des feuilles (les variables).
**Exemple avec $I I$ :**
$$
I = \lambda x.x \\
$$
$$
I_1 I_2=(\lambda x.\underline{x}) \underline{(\lambda y.y)}\\
\rightarrow_\beta(\lambda y.y)=I_2
$$

**Exemple avec $SKK$ :**
$$
S = \lambda x y z .(xz)(yz) \\
K = \lambda x y . x
$$
$$
SK_1K_2=(\lambda x y z .\underline{(xz)}(yz))\underline{K_1}K_2 \\
\rightarrow_\beta (\lambda y z . (K_1 z)\underline{(yz)})\underline{K_2} \\
\rightarrow_\beta (\lambda z . (\underline{K_1} z)(K_2z)) \\
\rightarrow_\beta \lambda z.((\underline{\lambda a b . a})\underline{z})(K_2z) \\
\rightarrow_\beta \lambda z.(\lambda b . z)(\underline{K_2}z) \\
\rightarrow_\beta \lambda z.(\lambda b . z)((\underline{\lambda a b . a})\underline{z})) \\
\rightarrow_\beta \lambda z.(\lambda b . \underline{z})(\underline{\lambda b . z}) \\
\rightarrow_\beta \lambda z.z \equiv I
$$

### Lambda to Ocaml

$(\lambda x.x)(\lambda y.y): T_1 \to T_1$

let ex1: 'a -> 'a = (fun x -> x) (fun y -> y);;

$SKK = (\lambda xyz.(xz)(yz)~\lambda xy.x)~(\lambda xy.x): T_1 \to T_1$

let ex2: 'a -> 'a = 
    let k = (fun x -> (fun y -> x)) in
    let s = (fun x -> (fun y -> (fun z -> (x z) (y z)))) in 
    s k k

$\Delta = \lambda x. x~x : ???$

let delta = (fun x -> x x) in
    delta delta

### Encodage

**Booléens:**
$T = \lambda xy.x$
$F = \lambda xy.y$
$ITE = \lambda abc. a\;b\;c$ (If a Then b Else c)
$$
ITE(T\;b\;c) = (\lambda abc. a~b~c)\lambda xy.x\;b\;c\to(\lambda y.b)\;c \to b \\
ITE(F\;b\;c) = (\lambda abc.a~b~c)\lambda xy.y~\;b\;c\to(\lambda y.y)\;c \to c
$$

$Not = \lambda x.x\;F\;T$
$$
Not(T) = (\lambda x.x\;F\;T)\;T \to (T\;F\;T) \to F
$$

$And = \lambda xy.x\;y\;F$
$$
And(T\;T) = (\lambda xy.x\;y\;F)\;T\;T \to (T\;T\;F) \to T\\
And(T\;F) = (\lambda xy.x\;y\;F)\;T\;F \to (T\;F\;F) \to F\\
And(F\;T) = (\lambda xy.x\;y\;F)\;F\;T \to (F\;T\;F) \to F\\
And(F\;F) = (\lambda xy.x\;y\;F)\;F\;F \to (F\;F\;F) \to F
$$

$Or = \lambda xy.x\;T\;y$
$$
Or(T\;F) = (\lambda xy.x\;T\;y)\;T\;F \to (T\;T\;F) \to T\\
Or(F\;F) = (\lambda xy.x\;T\;y)\;F\;F \to (F\;T\;F) \to F
$$

**Pairs:**
$(a,b) = \lambda x.ITE(x\;a\;b)$
$first = \lambda f.f\;T$
$second = \lambda f.f\;F$

$$
first (a,b) = (\lambda f.f\;T)\;\lambda x.ITE(x\;a\;b)
\to \lambda x.ITE(x\;a\;b)\; T
\to ITE(T\;a\;b)
\to a\\
second (a,b) = (\lambda f.f\;F)\;\lambda x.ITE(x\;a\;b)
\to \lambda x.ITE(x\;a\;b)\; F
\to ITE(F\;a\;b)
\to b
$$

**Entiers de Church**

$0 = \lambda fx.x$
$1 = \lambda fx.f\;x$
$2 = \lambda fx.f\;(f\;x)$
$3 = \lambda fx.f\;(f\;(f\;x))$
$n+1 = \lambda fx.f\;(n\;f\;x)$

et d'une manière générale : $n = λfx.f (f (...(f x)...)) = λfx.f^nx$ avec $f$ itérée $n$ fois.

Dans OCaml, un entier de Church a comme type **('a->'a)->'a->'a**

$succ = \lambda zfx.f\;(z\;f\;x)$
$$
succ\;0 = (\lambda zfx.f\;(z\;f\;x))\; \lambda ab.b\\
\to \lambda fx.f\;(\lambda ab.b\;f\;x)\\
\to \lambda fx.f\;x\\
\to 1
$$

$iszero = \lambda z.z\;(\lambda y.F)\;T$
$$
iszero\;0= (\lambda z.z\;(\lambda y.F)\;T)\;\lambda ab.b \\
\to (\lambda ab.b)\;(\lambda y.F)\;T \\
\to T
$$

$addition\;M\;N = \lambda fy.M\;f\;(N\;f\;y)$
$multiplication\;M\;N = \lambda f.M\;N\;f$

$$
1 + 1 = 2\\
1+1 = \lambda fy.(1\;f)\;(1\;f\;y)\\
\to \lambda fy.((\lambda ab.a\;b)\;f)\;(1\;f\;y)\\
\to \lambda fy.(\lambda b.f\;b)\;(1\;f\;y)\\
\to \lambda fy.f\;(1\;f\;y)\\
\to \lambda fy.f\;((\lambda ab.a\;b)\;f\;y)\\
\to \lambda fy.f\;(f\;y)\\
\to 2
$$

### Call-by-name vs Call-by-value
Parfois nous avons le choix pour appliquer la $\beta$-reduction.

Call-by-value (evaluer l'argument d'abord) :
$(\lambda z.z)((\lambda y.y)\;x) \to (\lambda z.z)\;x \to x$

Call-by-name (evaluer la fonction d'abord) :
$(\lambda z.z)((\lambda y.y)\;x) \to (\lambda y.y)\;x \to x$

### Parenthésage
Pour délimiter les applications, on utilise des parenthèses, mais par souci de clarté, on omet certaines parenthèses. Par exemple, on écrit x1 x2 ... xn pour ((x1 x2) ... xn).

### Typage

#### Règles de typage
$$
{\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}(VAR)
$$
$${\frac
{\Gamma ,x{\mathbin {:}}\sigma \vdash M{\mathbin {:}}\tau }
{\Gamma \vdash \lambda x{\mathbin {:}}M ~ {\mathbin {:}}~\sigma \to \tau }}(ABS)$$
$$
{\frac {\Gamma \vdash M{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash N{\mathbin {:}}\sigma }{\Gamma \vdash M~N{\mathbin {:}}\tau }} (APP)
$$
$$
{\frac {Γ ⊢ t_1:Bool \quad Γ ⊢ t_2:T \quad Γ ⊢ t_3:T} {Γ ⊢ if~t_1~then~ t_2~ else~ t_3~:T}}(ITE)
$$
$$
{\frac {Γ ⊢t_1 :T_1 \quad Γ,x:T_1 ⊢t_2 :T_2} {Γ ⊢let~x=t_1 ~in~t_2 :T_2}}(Let)
$$

#### Exemple
$K=\lambda xy.x$

Équations:
$T_1 = T_4$
$T_2 = T_3 \to T_4$
$T_0 = T_1 \to T_2$

Unification:
$T_0 = T_4 \to T_3 \to T_4$

Aussi égal à $~T_0 = T_4 \to (T_3 \to T_4)$

$S=\lambda xyz.xz(yz)$


\begin{align}
T_5 = T_9 \\
T_5 = T_{12} \\
T_1 = T_{12} \to T_{11} \\
T_3 = T_9 \to T_7 \\
T_{11} = T_7 \to T_6 \\
T_4 = T_5 \to T_6 \\
T_2 = T_3 \to T_4 \\
T_0 = T_1 \to T_2
\end{align}

\begin{align}
T_{11} = T_7 \to T_6 \\
T_4 = T_9 \to T_6 \\
T_0 = (T_9 \to T_{11}) \to ((T_9 \to T_7) \to T_4 )
\end{align}

\begin{align}
T_0 = (T_9 \to (T_7 \to T_6 )) \to ((T_9 \to T_7) \to (T_9 \to T_6) )
\end{align}

$SKK$

Pour typer $SK_1K_2$ plus facilement, on peut ne pas faire tous les arbres de dérivations.

Puisqu'on connait déjà les types de $S$ et $K$, on peut directement inférer le type de $SKK$ grâce à l'arbre de derivation ci dessus.

Donc les équations sont telles que :
$S = (A \to (B\to C))\to ((A \to B) \to (A \to C))$
$K = D \to E \to D$
$K = F \to G \to F$
Il faut bien différencier les deux $K$.

D'après la dérivation
$S = T_2 \to (T_1 \to T_0)$
$K_1 = T_2$
$K_2 = T_1$

Égalisons ces deux équations
$T_2 \to (T_1 \to T_0) = (A \to (B\to C))\to ((A \to B) \to (A \to C))$
$T_2 = D \to E \to D$
$T_1 = F \to G \to F$

Après unification on aura
$T_0 = A \to A$

#### Youtube Romain


## Références

### Bases
Traits impératifs ajoutés au lambda calcul simplement typé. Connus sous le nom de **"side effects"** ou **"computational effects"**.

Il y a 3 opérations basiques :
Allocation (=) , deréférencement (!), assignation (:=)

  r = ref 5;
> r : Ref Nat

  !r;
> 5 : Nat

  r := 7;
> unit: Unit

  !r;
> 7 : Nat

On peut imaginer **r** comme une **référence** ou un **pointeur** vers une cellule mémoire (r = ref 5;). On peut ainsi changer sa valeur, formellemement la valeur de la cellule pointée (r := 7). Par contre, pour faire des opérations avec **r**. Il faut le deréférencer (!r + 1).

### Alias
Plusieurs références peuvent pointer vers une même cellule

  r = ref 5;
> r : Ref Nat

  s = r;
> s : Ref Nat

  s := 7;
> unit: Unit

  !s = !r;
> bool = true

### Typage

## Java
### Lambda expression
### Surcharge
**Override ou redéfinition**
Quand une méthode avec le même nom et la même signature est défini dans la classe mère et la classe fille.

**Overload ou surcharge**
Quand une méthode a un même nom mais une signature différente (arguments différents).

À la compilation et à l'execution, on doit pouvoir choisir la méthode adéquate à appeler quand il y a surcharge de méthode.
Cet algorithme s'appelle la **résolution de surcharge**.

Exemple de surcharge en Java

public class Foo {
    public void doStuff(int y, String s) { }

    public void doStuff(int x)
    // Valid overload as DIFFERENT ARGUMENT LIST
    // (and methods can be overloaded
    // in the same class or in subclass)
}

class Bar extends Foo {

    private void doStuff(long a)
    // Valid overload as DIFFERENT ARGUMENT LIST
    // (access modifier CAN be same or different)

    public String doStuff(int y, String s)
    // Invalid overload, MUST change method's
    // argument list (compiler error)
        
    public static void doStuff(int x)
    // Invalid overload, MUST change method's
    // argument list (compiler error) 
}

La seule règle qu'on doit respecter est de **changer les arguments**, le reste est optionel.

#### Invocation des méthodes surchargées

public class Animal

class Horse extends Animal

class UseAnimals {
    public void doStuff(Animal a) {
        System.out.println("In the Animal version");
    }

    public void doStuff(Horse h) {
        System.out.println("In the Horse version");
    }

    public static void main(String[] args) {
        UseAnimals ua = new UseAnimals();
        Animal animalObj = new Animal();
        Horse horseObj = new Horse();
        Animal animalRefToHorse = new Horse();

        ua.doStuff(animalObj);
        ua.doStuff(horseObj);
        ua.doStuff(animalRefToHorse);
    }
}

Résultats

In the Animal version
In the Horse version
In the Animal version

Remarquons l'appel `doStuff(animalRefToHorse)`, ici la version `Animal` de `doStuff` est appelée. En effet, c'est le **type de référence (ici Animal =)** qui détermine la méthode à appeler.

Pour résumer, le choix de la méthode redéfinie se fait à l'execution; le choix de la méthode surchargée se fait à la compilation.

### Ordre de priorité pour les méthodes surchargées

Le choix du compilateur se fait comme suit (par ordre de préférence):
- Widening
- Autoboxing
- Var-args

public class MethodOverloading {

    static void go(float x) {
        System.out.print("float ");
    }

    static void go(Long x) {
        System.out.print("Long ");
    }

    static void go(double x) {
        System.out.print("double ");
    }

    static void go(Double x) {
        System.out.print("Double ");
    }

    static void go(int x, int y) {
        System.out.print("int,int ");
    }

    static void go(byte... x) {
        System.out.print("byte... ");
    }

    static void go(Long x, Long y) {
        System.out.print("Long,Long ");
    }

    static void go(long... x) {
        System.out.print("long... ");
    }

    public static void main(String[] args) {
        byte b = 5;
        short s = 5;
        long l = 5;
        float f = 5.0f;
        // widening beats autoboxing
        go(b);
        go(s);
        go(l);
        go(f);
        // widening beats var-args
        go(b, b);
        // auto-boxing beats var-args
        go(l, l);
    }
}

Résultat `float float float float int,int Long,Long`.

La JVM préfère le `widening` que les `autoboxing et var-args`. Dans le cas où un match exact n'est pas trouvé, elle utilise la méthode avec l'argument qui se rapproche le plus (en terme de sous-typage) des paramètres.

## Ocaml
### Bases
#### Déclarations
**Variables**
Plus généralement, un programme OCaml est constitué d'une suite quelconque d'expressions à évaluer et de déclarations, séparées par un double point-virgule `;;`. Une déclaration affecte le résultat de l'évaluation d'une expression à une variable, et est introduite par le mot clé `let`. Ainsi le programme suivant :

let x = 1 + 2;;
print_int x;;
let y = x * x;;
print_int y;;

calcule le résultat de 1+2, l'affecte à la variable x, affiche la valeur de x, puis calcule le carré de x, l'affecte à la variable y et en affche la valeur de y.

**Fonction**
La syntaxe d'une déclaration de fonction est conforme à la syntaxe de son utilisation. Ainsi

let f x = x * x;;

Définit une fonction f ayant un unique argument x et retournant son carré.
#### Références
Si l'on souhaite utiliser une variable mo diable en place, il faut l'intro duire à l'aide du mot clé supplémentaire ref :

let x = ref 1;;

#### Boucles
**For**

for i = 1 to 10 do x := !x + i done

#### if

if !x > 0 then x := 0

### Implémentations de différents $\lambda$ calcul en Ocaml
**L'identité :**

*$\lambda$ calcul :*
>$$
\lambda x . x
$$

*Ocaml :*

let I = fun x -> x ;;

**Entier Church :**

let rec entierChurch (n : int) =
    fun f z -> if n = 0 then z else f ((entierChurch (n-1)) f z)
;;

### Structures de données en Ocaml

#### **Listes :**
Pour construire des listes (simplement chaînées), on a besoin d'une valeur pour la liste vide, `listevide`, d'un constructeur pour une liste `cons`, un prédicat pour la liste vide `estvide`, un accesseur `tete` et `queue`, et avec les contraintes suivantes :

estvide (listevide) == vrai
estvide (cons tt qu) == faux
    
tete (cons tt qu) == tt
queue (cons tt qu) == qu

On va stocker tout ça avec des fonctions qui attendront deux arguments (deux fonctions - rappel tout est fonction en $\lambda$-calcul), l'une appellée si la liste est vide, l'autre si la liste n'est pas vide.

let listevide = fun survide surpasvide -> survide;;

*Out :* ` val listevide : 'a -> 'b -> 'a = <fun>`

let cons = fun hd tl -> fun survide surpasvide -> surpasvide hd tl;;

*Out :* `val cons : 'a -> 'b -> 'c -> ('a -> 'b -> 'd) -> 'd = <fun>`

Avec cette construction, `estvide` est assez simple : `survide` est `() -> vrai` et `surpasvide` est `tt qu -> faux`.

let estvide = fun liste -> liste (vrai) (fun tt qu -> faux);;

*Out :* `val estvide : (('a -> 'b -> 'a) -> ('c -> 'd -> 'e -> 'f -> 'f) -> 'g) -> 'g =
<fun>`

Les deux extracteurs :

let tete = fun liste -> liste (vide) (fun tt qu -> tt);;
let queue = fun liste -> liste (vide) (fun tt qu -> qu);;

**Utilisation :**

cons un (cons un listevide);; (* 8 variables pour une liste de taille 2 *)

*Out :*

'_a ->
    ((('_b -> '_b) -> '_b -> '_b) ->
        ('_c ->
            ((('_d -> '_d) -> '_d -> '_d) -> ('_e -> '_f -> '_e) -> '_g) ->               '_g) ->
        '_h) ->
    '_h
= <fun>

#### Arbres binaires

**Structure** :

type 'a arbre_bin =
  | Fin
  | Noeud of 'a * 'a arbre_bin * 'a arbre_bin

**Profondeur** :

let rec prof (arb : 'a arbre_bin) : int =
  match arb with
  | Fin -> 0
  | Noeud(_, enfant1, enfant2) ->
    (* On utilise la fonction standard max *)
    1 + (max (prof enfant1) (prof enfant2))

**Somme :**

let rec somme (arb : int arbre_bin) : int =
  match arb with
  | Fin -> 0
  | Noeud(x, enfant1, enfant2) -> x + (somme enfant1) + (somme enfant2)

**Appartient :**

let appartient (x : 'a) (l : 'a l) : bool =
  match l with
  | [] -> false
  | elem :: suite -> (elem = x) || (appartient x suite)

**Implémentation de la double file**

type 'a file = File of 'a list * 'a list;;

let enqueue f e =
  let (entrant,sortant) = f in
  (e::entrant, sortant);;

let copyover f =
  let (entrant, _) = f in 
  let rec loop s = function 
      [] -> s
    | t::q -> loop (t::s) q
  in
  ([], t::q) -> t;;

let rec dequeue = function
    ([], []) -> failwith "liste vide"
  | (l, []) -> dequeue (copyover (l, []))
  | (_, t::q) -> t;;

**Typage dans une classe**

get_nom: string
to_string: unit -> string
eq: 'a -> bool


`point_colore :> point` point_colore est sous-type de point.

### <ins>Exercice Surcharge :</ins>

class A {
    void m(B x) { /* A1 */ }
    void m(C x, B y) { /* A2 */ }
}
class B extends A {
    void m (A x) { /* B1 */}
    void m (B x , A y) { /* B2 */ }
    void m (C x , B y) { /* B3 */ }
}
class C extends B {
    void m (C x) { /* C1 */ }
    void m (C x, C y) { /* C2 */ }
    void m (C x, B y) { /* C3 */ }
}

class D {
    public static void main(String[] args) {
        A a = new A();
        B b = new B();
        A a1 = b;
        C c = new C();
        B b1 = c;
        A a2 = b1;
        
        // QUESTION 1
        a.m(b); // m(B) - A1
        a.m(a1); // clash
        b.m(a1); // m(A) - B1
        b.m(b); // m(B) - A1
        c.m(c); // m(C) - C1
        c.m(b1); // m(B) - A1
        
        // QUESTION 2
        a.m(b,b); // clash
        a.m(c,c); // m(C, B) - A2
        a.m(c,b); // m(C, B) - A2
        b.m(b,b); // m(B, A) - B2
        b.m(c,c); // m(C, B) - B3
        b.m(c,b1); // m(C, B) - B3
        c.m(b,b);  // m(B, A) - B2 *
        c.m(c,c);  // m(C, C) - C2
        c.m(c,b1); // m(C, B) - C3
        
        // BONUS
    /* Le choix de la fonction à appeler 
     * se fait sur la référence (ici b1 pointe sur C),
     *  les arguments par contre doivent bien matcher
     *  le type ici (C, B) */
        b1.m(c, b1); // m(C, B) - C3 
        a1.m(c, c); // m(C, B) - B3
        a2.m(c, c); // m(C, B) - C3
    }
}

### Annale 2018