Table of Contents
LANGAGES ET TRADUCTEURS – Chapitre 1 Pierre Corbineau, 2025
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