.. include:: ../../tronCommun/fonctions.txt

Définitions par filtrage
--------------------------

::

    type formule = Vrai | Faux | Conjonction of formule * formule


le fitrage permet un examen par cas sur les valeurs construites::

    let rec evalue = function
        | Vrai -> true
        | Faux -> false
        | Conjonction (Faux, _) | Conjonction (_, Faux) -> false
        | Conjonction (f1, f2) -> evalue f1 && evalue f2;;


Lorsqu'un argument est passé à un ensemble de clauses :

- la première clause qui filtre l'argument est exécutée, les autres sont
  ignorées.
- si aucune clause ne filtre l'argument, une exception est levée.

exemple de définition par cas
::

	let points v =
        match v with
             Pique -> 1
            | Trefle -> 2
            | Coeur -> 3
            | Carreau -> 4;;

	# points a ;;
	- : int = 2


Définitions récursives
-----------------------

En ocaml, `let rec` définit une variable récursive, ie qui utilise la (les) valeur(s) en cours de définition.

Exemples
--------

::

	let rec f (x) = if x <= 1 then 1 else f(x-1) + f(x-2) ;;
	let rec g (x) = if x = 0 then 1 else x * g (x-1) ;;
	let rec h (x, y) = if x = 0 then 1 else h (x-1, h(x,y)) ;;
	let rec m (x) = if x > 100 then x - 10 else m (m (x+11)) ;;

On peut imprimer leur valeurs pour qques valeurs::

	begin
	for i = 1 to 15 do
	   printf "%d " (f(i)) done;
	   printf "\n"
	end ;;

f, g sont les fonctions de Fibonacci et factorielles. C'est la même notation que pour les suites récurrentes. Que valent h et m ?

La récursivité est très puissante. Invention de Kleene (1935). Théorie des fonctions récursives, comme moyen général de calcul.
On peut montrer qu'il existe toujours des fonctions récursives partielles (qui ne terminent pas pour tte valeur de leurs arguments), si on veut un modèle général. La sous théorie des fonctions récursives primitives correspond aux programmes sans boucles, sans appels récursifs, et l'instruction for. Ces programmes terminent toujours. (cf Introduction to Metamathematics, S. Kleene; Recursive Functions Theory and Logic, A. Yasuhara).

Church et les autres logiciens des années 30 ont montré que systèmes de Post, les fonctions récursives de Kleene, les machines de Turing, sont tous équivalentes. Il a émis la thèse suivante: tous les modèles de la calculabilité sont équivalents.



Fonctions récursives
---------------------

::

    let rec fact n = if n > 1 then n * fact (n -1) else 1;;

dans le prompt::

    utop # let rec fact n = if n > 1 then n * fact (n -1) else 1;;
    utop # fact 5;;
    - : int = 120

et mutuellement récursives::

    let rec ping n = if n > 0 then pong (n - 1) else "ping"
        and pong n = if n > 0 then ping (n - 1) else "pong";;


    # ping 8 ;;
    - : bytes = "ping"
    #  ping 15 ;;
    - : bytes = "pong"

types récursif
---------------

::

    type 'a liste =
      Vide
      | Cellule of 'a * 'a liste;;