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

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

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

• Représentation des entiers de Peano: \[ \textrm{nat_peano} = \{O\}\cup\{S(n) | n \in \textrm{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}\rightarrow\textrm{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: $\rightarrow$ démo live.

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

• Spécification add
  • profil: $\textrm{nat_peano}\rightarrow\textrm{nat_peano}\rightarrow\textrm{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
    • $\forall\textrm{x},\quad$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:$\rightarrow$ démo live.

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

• Terminaison:$\rightarrow$ 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:$\rightarrow$ démo live.
• Complexité: $\sim \log n$

• profil: $\mathbb{N}\rightarrow\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:$\rightarrow$ démo live.
• Terminaison: mesure p q = min(p,q)