Currification

Exercice

Montrer que la formule suivante est valide / prouvable : (A → (B → C)) ↔ (A ∧ B → C) Remarque: → est associatif à droite, on aurait pu écrire: (A → B → C) $↔(A ∧ B → C)

currification

La curry cation consiste à transformer une fonction qui prend plusieurs arguments en une fonction qui prend un seul argument et qui retourne une fonction qui prend en arguments les arguments restants.

Pourquoi utiliser la curry cation ? Afi n de pouvoir réaliser des applications partielles plus facilement.

Remarque: cette opération porte le nom de Haskell Curry (1900-1982).

Exemple

En Caml Au lieu d'écrire:

# let f(x,y) = x + y;;
val f : int * int -> int = <fun>

On écrit:

# let f x = fun y -> x + y;;
val f : int -> int -> int = <fun>

ou bien

# let f x y = x + y;;
val f : int -> int -> int = <fun>

Exemple

En Coq On utilise la curry cation quand on écrit des fonctions ou des théorèmes.

On écrira plutôt:

Lemma toto: forall p q : R, p > 0 -> q > 0 -> p*q > 0.

que:

Lemma toto: forall p q : R, p > 0 /\ q > 0 -> p*q > 0.

curry & unCurry

Comment faire “curry” et “uncurry”?

let curry f (A*B->C) = function x -> function y -> f(x,y)

let uncurry f(A->B->C) = function(x,y)-> f x y

Lien avec les preuves :

Lemma curry_prop : forall A B C : Type, (A*B -> C) -> A -> B -> C.
Proof.
intros A B C f x y
apply f.
split.
apply x.
apply y.
Defined.
Print curry_prop.
curry_prop =
  fun (A B C:Type) (f:A*B->C) (x:A)(y:B)=>f(x,y) :
    forall A B C:Type,
    (A * B -> C) -> A -> B -> C
 
m1ilc/preuves_3.txt · Dernière modification: 2010/05/19 08:55 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki