Récursivité dans $\mathbb{N}$

• Fonction fact $\to$ démo live.

• 
  	  let rec fact (n:int):int = match n with
  	  |0 -> 1
  	  |_ -> n*(fact (n-1))
  	  ;;
        

• Représentation des entiers de Peano: $$\text{nat\_peano}=\{O\}\cup \{S(n)|n\in \text{nat\_peano}\}$$

• 
  	  type nat_peano = O | S of nat_peano;;
        

On distinguera deux concept clés dans la réalisation d'une fonction:

• La Spécification
  • Abstrait
  • Précis
  • Proche d'une description mathématique
  • Contient des exemples représentatifs
• La Réalisation
  • Algorithme en Français
  • Algorithme en OCaml

• Spécification
  • profil: $\mathbb{N}\to \text{nat\_peano}$
  • sémantique: int_v_int_peano(n) est le naturel de Peano correspondant à l'entier $n$.
  • exemples:
    • int_v_int_peano(0)=O
    • int_v_int_peano(4)=S(S(S(S O)))
• Réalisation
  • équation de récurrence:
    • int_v_int_peano(0)=O
    • int_v_int_peano(p+1)=S(int_v_int_peano(p))
  • implémentation: $\to$ démo live.

• Terminaison
  Montrer que pour tout $n$ dans $\mathbb{N}$ la fonction int_v_nat_peano termine.
  $\to$ démo live.

• Spécification add
  • profil: $\text{nat\_peano}\to \text{nat\_peano}\to \text{nat\_peano}$
  • sémantique: add n1 n2 est le naturel de Peano correspondant à la somme des entiers $n_1$ et $n_2$.
  • exemples:
    • add O O=O
    • $\mathrm{\forall }\text{x},$add x O = x
    • add S(O) S(O) = S (S O))
• Réalisation
  • équation de récurrence ?

		add O O = O
		add S(x) O = S(x)
		add O S(y) = S(y)
		add x S(y) = S(add x y)
		add x S(y) = add S(x) y)
		add S(x) y = S(add x y)
		add S(x) y = add x S(y)
		add S(x) S(y) = S(S(add x y))
	    

		add O O = O
		add S(x) O = S(x)
		add O S(y) = S(y)
		add x S(y) = S(add x y)
		add x S(y) = add S(x) y)
		add S(x) y = S(add x y)
		add S(x) y = add x S(y)
		add S(x) S(y) = S(S(add x y))
	    

		add O O = O
		add S(x) O = S(x)
		add O S(y) = S(y)
		add x S(y) = S(add x y)
		add x S(y) = add S(x) y)
		add S(x) y = S(add x y)
		add S(x) y = add x S(y)
		add S(x) S(y) = S(S(add x y))
	    

		add O O = O
		add S(x) O = S(x)
		add O S(y) = S(y)
		add x S(y) = S(add x y)
		add x S(y) = add S(x) y)
		add S(x) y = S(add x y)
		add S(x) y = add x S(y)
		add S(x) S(y) = S(S(add x y))
	    

		add O O = O
		add S(x) O = S(x)
		add O S(y) = S(y)
		add x S(y) = S(add x y)
		add x S(y) = add S(x) y)
		add S(x) y = S(add x y)
		add S(x) y = add x S(y)
		add S(x) S(y) = S(S(add x y))
	    

• Implémentation:$\to$ démo live.

• Spécification
  • profil: $\text{puissance}:\mathbb{R}\to \mathbb{N}\to \mathbb{R}$ ou $\text{float}\to \text{int}\to \text{float}$
  • sémantique: Élève un réel à la puissance $n$
  • exemples:
    • $\text{puissance}(x,0)=1$
    • $\text{puissance}(2,2)=4$
    • $\text{puissance}(-1,3)=-1$
• La Réalisation
  • $\text{puissance}(x,0)=1$
  • $\text{puissance}(x,n)=x\times \text{puissance}(x,n-1)$
  • Implémentation:$\to$ démo live.

• Terminaison:$\to$ démo live.
• Complexité: Combien d'appel à la fonction ?

Possible de faire mieux ?

• $x^{2n}=x^n\times x^n$
• $x^{2n+1}=x^n\times x^n\times x$
• Implémentation:$\to$ démo live.
• Complexité: $\sim \log n$

• profil: $\mathbb{N}\to \mathbb{N}$
• sémantique: mult x y = x*y
• exemple: mult x 0 = 0
• équations récursives:
  • mult 0 0 = 0
  • mult 0 p = 0
  • mult q 0 = 0
  • mult p q = (mult (p-1) (q-1)) + p + q - 1
• Implémentation:$\to$ démo live.
• Terminaison: mesure p q = min(p,q)