Langages et Traducteurs – Chapitre 1 - Préliminaires sur les fonctions

(vu rapidement au CM de PF) En programmation fonctionnelle, on a des fonctions anonymes

1 Syntaxe

1.1 OCaml

(fun x -> (1 + x) * 3)            : int -> int
fun x -> fun y -> (1 + x) * y     : int -> int -> int
fun x -> (fun y -> (1 + x) * y)   : int -> (int -> int)

Comprendre : fun x -> (fun y -> (1 + x) * y)
Les arguments seront appliqués successivement

(((fun x -> (fun y -> (1 + x) * y)) 20) 2)
(let x = 20 in (fun y -> (1 + x) * y)) 2
(fun y -> let x = 20 in (1 + x) * y) 2
(let y = 2 in let x = 20 in (1 + x) * y)
(42)

fun (x, y) -> (1 + x) * y       : int * int -> int

UN argument de type couple

1.2 Rocq

fun x => (1 + x) * 3                  : nat -> nat
fun x => fun y => (1 + x) * y         : nat -> nat -> nat

Comprendre : fun x => (fun y => (1 + x) * y)

NB : en Rocq on a des entiers naturels mathématiques, commençant en 0 et non bornés, d'où nat au lieu de int.

2 Application d'une fonction à un argument

2.1 OCaml

(fun x -> (1 + x) * 3) 4
(fun (x, y) -> (1 + x) * y)  (2, 5)  (* *1* argument qui est un couple *)

2.2 Rocq

(fun x => (1 + x) * 3) 4

3 Application d'une fonction à deux arguments

3.1 OCaml

((fun x -> fun y -> (1 + x) * y) 2) 5

Notation raccourcie

(fun x -> fun y -> (1 + x) * y) 2 5

Notation encore plus raccourcie

(fun x y -> (1 + x) * y) 2 5

3.2 Rocq

((fun x => fun y => (1 + x) * y) 2) 5

4 On n'y voit rien ! Donnons un nom aux fonctions

4.1 OCaml

let f = fun x -> fun y -> (1 + x) * y;;

(f 2) 5

Plus simplement :

f 2 5

4.2 Rocq

Definition f := fun x => fun y => (1 + x) * y.
Definition f := fun x y => (1 + x) * y

(f 2) 5

Plus simplement :

f 2 5

∼∼∼

Made with Org-mode