Table of Contents
LANGAGES ET TRADUCTEURS – Chapitre 1 Jean-François Monin, 2021
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
Comprendre : fun x -> (fun y -> (1 + x) * y) Les arguments seront appliqués successivement
fun (x, y) -> (1 + x) * y : int * int -> int UN argument de type couple
1.2 Coq
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 Coq 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 Coq
(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
3.2 Coq
((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 Coq
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