Définition fonction

Je trouve le sujet soulevé par Foys franchement, assez génialement, essentiel.

Cela fait longtemps que je n'avais pas réfléchi à ce qu'était une chose abstraite. Qu'est-ce qu'une abstraction ?
Modulo la dérive péjorative grossière et intellectuellement pauvre, on peut dire que le sens général donné à une chose abstraite, ou à l'abstraction, est que c'est une chose qui relève de l'action d'abstraire.
C'est quoi, abstraire ? C'est :

TLFi a écrit:

Isoler, par l'analyse, un ou plusieurs éléments du tout dont ils font partie, de manière à les considérer en eux-mêmes et pour eux-mêmes.

Au fond, c'est la pratique quotidienne du matheux, ça devrait être son pain quotidien, non ? Abstraire. Isoler.

On peut bien isoler le calcul dans Z du calcul dans Q, non ? Est-ce que la notion de corps des fractions est abstraite ? Oui. Est-ce que ce travail d'abstraction est nécessaire pour comprendre le calcul dans Q ? Oui.

L'abstraction, c'est la distinction. C'est la coloration de la vue. C'est l'anti-daltonisme intellectuel.

C'est essentiel. C'est le travail du prof de maths.

Sauf erreur de ma part, les questions du type
"Donner l'ensemble de définition de la fonction tartempion définie par ..." ont enfin disparu du champ de vision de l'éducnat. Bien entendu on déplore une pollution persistante de la part d'un corpus résiduel d'exercices en circulation de la part de profs qui se les recopient libéralement.

Pour ton copain, ma réponse est - je reste dans le cadre civilisé des fonctions numériques d'une variable réelle - n'importe quoi, pourvu que tu n'aies pas la déveine cosmique d'y coller zéro dedans.

Elle est pas belle ma phrase ?

e.v.

Bonsoir,

Foys a écrit:

l'ensemble de définition de $x\mapsto 2+\dfrac{4}{x}$ dans un corrigé pour ses secondes

Ce n'est pas très compliqué.
Il y a une différence entre une réponse pour logicien tatillon qui prépare une thèse sur le sujet (ce qui ne m'intéresse pas) et une réponse adaptée à des élèves de seconde.
Par exemple, on peut dire que c'est l'ensemble des nombres réels $x$ pour lesquels l'expression a un sens.
En seconde ça suffit.
Bien sûr, on peut pinailler:
On peut définir une fonction par $x\mapsto 2+\dfrac{4}{x}$ sur $[3;4]$ et autre chose (ou non définie) ailleurs, mais ce n'est pas naturel pour un élève.
En l'absence de précision, on prendra l'ensemble maximal (pour l'inclusion).
Et bien sûr, en seconde, on se "contente" de $\mathbb{R}$.

Cordialement,

Rescassol

Non, ce n'est pas vraiment niveau 3ème.

ev a écrit:

Par ailleurs, j'ai jeté un coup d'oeil sur la prose de Foys s'évertuant à expliquer que la notion de fonction n'avait rien de mystérieux. Quand je suis tombé sur " Couple(d,a,b)", j'ai dû rebooter mon pacemaker avant qu'il ne fasse office de moulin à poivre.

Ce message était plutôt une réponse à une remarque de Titi le curieux dans l'autre fil. Il semblait suggérer que constuire des fonctions sans cercle vicieux était impossible ("il me faut la paire" etc). Il s'agit surtout d'expliquer que certaines choses sont des commodités de lecture et non des besoins indispensables pour des motifs de fondements.
Pour une version tout public je le réécrirais différemment je pense.

Rescassol a écrit:

Par exemple, on peut dire que c'est l'ensemble des nombres réels x pour lesquels l'expression a un sens.

On propose ci-dessous un petit programme en coq abordant cette problématique.
NB: même si ce n'est pas la version la plus récente, je suis entièrement persuadé que le comportement potentiellement perçu comme inadéquat se retrouve dans les versions ultérieures (n'envoyez pas de mails d'indignation à la coq team, ce n'est PAS un bug.)
Plus de détails lundi, je vais être très occupé ce week-end.

foys@chez_foys:~/Documents/codage/coq$ coqc inverse_rescassol.v
fonction_sec ([0 ]°)
     : K
[2 ]° +° [4 ]° /° [0 ]°
     : K

(*2019/03/30*)
(*Ce programme compile avec COQ 8.7*)

Require Import Field.

Section main.

  Variable K:Type.
  Variables K_0 K_1:K.
  Variables K_plus K_mult K_sub K_div: K -> K -> K.
  Variables K_opp K_inv: K -> K.

  Hypothesis K_est_un_corps:
   @field_theory K K_0 K_1 K_plus K_mult K_sub K_opp K_div K_inv eq.

  (*On introduit des notations plus familières pour les opérations, avec les bonnes
priorités*)
  Notation "~° a" := (K_opp a) (at level 11).
  Notation "a ^°(-1)" := (K_inv a) (at level 11).
  Notation "a /° b" := (K_div a b) (left associativity, at level 21).
  Notation "a *° b" := (K_mult a b) (left associativity, at level 21).
  Notation "a -° b" := (K_sub a b) (left associativity, at level 31).
  Notation "a +° b" := (K_plus a b) (left associativity, at level 31).
  
  (*On plonge les entiers dans K*)
  Fixpoint int_to_K (n:nat):K:=
    match n with
    |0 => K_0
    |S m => K_1 +° (int_to_K m)
    end.

  Notation "[ n ]°" := (int_to_K n) (at level 10).
  
  Add Field Kfield: K_est_un_corps.
  (*pour pouvoir utiliser les "tactiques" (procédures automatiques) de COQ pour les calculs
dans un corps*)
  
  Lemma test_calcul: forall x y z:K,
      z <> K_0 ->
      (x +° y)/° z = (x /° z) +° (y /° z).
    Proof.
      intros.
      field.
      assumption.
    Qed.
    (*tout semble marcher normalement*)

    Definition fonction_sec (x:K) := [ 2]° +°  [4]° /° x.
    (*apparemment l'ensemble de définition n'est pas demandé*)

    (*quelques tests:*)

    (*K_0 est bien zéro*)

    Lemma zero: forall x:K, (K_0 +° x = x) /\ (x = x +° K_0) /\ [0]° = K_0.
    Proof.
      intros.
      split.
      field.
      split.
      field.
      simpl.
      reflexivity.
    Qed.

    (*Les fractions ont un comportement normal*)
    Lemma frac: forall x y:K,
        x <> [0]° ->
        y <> [0]° ->
        (x /° y) *° (y /° x) = [1]°.
    Proof.
      assert (K_1 +° K_0 = K_1).
      field.
      intro.
      intro.
      simpl.
      intros.
      rewrite H.
      field.
      split.
      assumption.
      assumption.
    Qed.
    
    Lemma calcul_1: fonction_sec( [1]°) = [6]°.
    Proof.      
      unfold fonction_sec.
      simpl.
      field.
      apply K_est_un_corps.
    Qed.

    Lemma calcul_2: fonction_sec (~° [1]°) = ~° [2]°. 
    Proof.      
      unfold fonction_sec.
      simpl.
      field.
      simpl.
      intro.
      assert (K_1 = K_0).
      apply eq_trans with (y:= ~° K_1 *° ~° K_1).
      field.
      rewrite H.
      field.
      cut (K_1 = K_0).
      apply K_est_un_corps.
      assumption.
    Qed.

    Lemma calcul_y: forall (y:K),
        y <> [0]° -> y *° (fonction_sec y) = [2]° *° y +° [4]°.  
    Proof.
      unfold fonction_sec.
      intro.      
      simpl.
      intro.
      field.
      assumption.
    Qed.

    (*fonction_sec est la fonction x -> 2+4/x sur le corps K*)

    (*Or ceci ne provoque pas de message d'erreur*)

    Check (fonction_sec ([0]°)).

    (*En fait ceci non plus*)

    Check ([2]° +° [4]°/° [0]°).

    Theorem surprise:
      (fonction_sec([0]°) <> [0]°) ->
      (fonction_sec ([0]°)) *° (fonction_sec([0]°))^°(-1) = [1]°.
    Proof.
      intros.
      simpl.
      assert (K_1 +° K_0 = K_1).
      field.
      rewrite H0.
      field.
      simpl in H.
      assumption.
    Qed.
    (*vous avez bien lu, COQ accepte et valide des théorèmes parlant de f(0) 
      où f= fonction_sec*)

    (*ah, et on a aussi*)

    Theorem surprise2: forall x:K,
        (x /° [0]° <> [0]°) ->   (x /° [0]°) *° (x /° [0]°)^°(-1) = [1]°.
    Proof.
      intro.
      simpl.
      intro.
      assert (K_1 +° K_0 = K_1).
      field.
      rewrite H0.
      assert (forall u, u <> K_0 -> u *° (u^°(-1)) = K_1).
      intros.
      field.
      assumption.
      apply H1.
      assumption.
    Qed.

    (*un théorème qui annonce que pour tout x, si (x/0) est non nul alors
     (x/0)*(x/0)^-1 = 1. C'est juste un corollaire de ce que pour tout u non nul,
     u * u^-1 = 1*)
      
End main.

Pour en revenir à la "définition" de fonction niveau collège :

(1) La vraie définition comme ensemble de couples ne me semble pas abordable. Si on dit «soit $f(x)=\dfrac{1}{(1+x)^3}$», je ne vois pas un ensemble de couples mais une formule qui me permet de calculer $f(x)$ connaissant $x$.
On imagine mal un collégien pensant que $(4,2)\in\sqrt{\phantom{a}}$, voire que $\{4,\{4,2\}\}\in\sqrt{\phantom{a}}$.

(2) La fausse définition disant qu'une fonction est un procédé prenant en entrée un nombre $x$ et calculant un nombre $f(x)$ ne dépendant que de $x$ est plus proche de la quasi-totalité des exemples vus dans le secondaire. La difficulté est que deux algorithmes différents peuvent donner la même fonction.

Il me vient alors une autre idée. On ne définit pas ce qu'est une fonction mais on explique le mode d'emploi : si $f$ est une fonction et $x$ est un nombre appartenant à l'ensemble de définition de $f$ (ensemble de valeurs autorisées), alors

(a) $f(x)$ est un nombre qui dépend uniquement de $x$ (et de la fonction $f$)
(b) deux fonctions $f$ et $g$ sont égales si elles ont le même ensemble de définition, et si $f(x)=g(x)$ pour tout $x$.

Exemples :

* $x$ est le nombre de secondes écoulées depuis le 1er janvier 0h00, $f(x)$ est la température de la salle de classe à l'instant $x$.
* $f(x)=(x+1)^2$, $g(x)=x^2+2x+1$. Alors $f=g$.

Math Coss a écrit:

Mettre une boîte noire autour du « procédé » reviendrait à quotienter par les différentes formules qui définissent la même fonction.

1° Le problème est que savoir si étant donné deux expressions $F,G$ (on va noter dans ce paragraphe $\Phi(E)$ la fonction définie par $E$), savoir si pour tout $x$ $\Phi(F)(x)$ et $\Phi(G)(x)$ renvoient la même chose (i.e. rien ou le même résultat), est en général un problème indécidable.

2° Dans des formalismes comme les théories de types (comme COQ) où in fine la notion de fonction est première (en gros (*)si $A,B$ sont des types, vous avez un type $A\to B$ qui tombe du ciel et on considère que pour tous objet $m$ de type $A$ et tout objet $j$ de type $A\to B$, $j(m)$ est un objet de type $B$ and that's it), l'égalité entre fonctions $f,g$ est par définition l'égalité des termes après simplification des expressions donnant $f$ et $g$ (et dans COQ ce calcul termine toujours). Quant à l'autre notion d'égalité plus classique (on va dire "extensionnelle": celle de mon 1°) vous n'avez parfois aucun moyen de savoir si elle est satisfaite ou non.

Finalement on peut penser que (*) est la définition la plus intuitive (ou la plus dépouillée) mais elle traîne des problèmes subtils derrière elle.

Noter aussi que dans (*) un objet de type $A\to B$ est toujours défini sur la totalité de $A$.

Oui mais $x\mapsto \frac{1}{x}$ ?

Ca va être l'occasion de dire un peu de mal (argumenté) de ces "ensembles de définition".
La mauvaise nouvelle est que savoir si un terme s'annule est en général indécidable.
Vous avez besoin qu'il soit toujours possible de savoir si l'objet syntaxique $f$ est dans le type $A\to B$, mais vous voudriez conditionner cette vérification à la résolution préalable d'un problème de difficulté potentiellement illimitée, voire indécidable.

La détermination des "ensembles de définition de $x \mapsto \frac{1}{x+9}$ et $x \mapsto 5+\frac{2}{x^2+2x+4}$" amène en général des réponses consensuelles (indépendamment de ce que les gens pensent des ensembles de définition).

Mais déjà pour $x \mapsto \frac{1}{x^5-3x+1}$, Galois apparaît.
L'ensemble de définition de cette chose ne s'exprime plus avec des symboles mathématiques connus ce qui amène à interroger la pertinence de l'expression "ensemble de définition".

En fait, on a carrément ceci:
https://en.wikipedia.org/wiki/Diophantine_set#Matiyasevich's_theorem

I) Soit $X$ une partie de $\N$. Les énoncés suivants sont équivalents ("Théorème de Matyasevic").

(i) $X$ est l'image de $\N$ par une fonction calculable (i.e. un programme informatique-en faisant abstraction des limites physiques -RAM etc. Autrement dit un programme tournant "indéfiniment" vous livre successivement $x_0,x_1,x_2,x_3...$ et $X=\{x_n \mid n \in \N\}$).

(ii) Il existe un programme informatique prenant en argument un entier, et tel que $X$ est exactement l'ensemble des entrées sur lesquelles ce programme s'arrête.

(iii) il existe un entier $d$ et un polynôme $P(X_0,X_1,...,X_d)$à $d+1$ indéterminées et à coefficients entiers relatifs, tel que $X$ est exactement l'ensemble des entiers $n$ pour lesquels l'équation en $x_1,...,x_d$: $$P(n,x_1,...,x_d)$$ a au moins une solution entière.

Un ensemble $X$ satisfaisant ces conditions équivalentes est dit récursivement énumérable.

(i) <=> (ii) et (iii) =(ii) sont des exos intuitifs (cf cours de calculabilité/fonctions récursives).
(i) =>(iii) est non trivial et a valu une renommée méritée à son auteur.

Par exemple l'ensemble des théorèmes de ZFC (ou n'importe quelle théorie formalisable) est (après encodage des énoncés dans les entiers) un ensemble récursivement énumérable.
Nommons $R$ le polynôme à $k+1$ variables correspondant à ce cas particulier.

Donc vous avez une équation diophantienne $Q(x_1,...,x_k)=0$ qui a des solutions si et seulement si l'hypothèse de Riemann est prouvable ($Q(...) = R(m,...)$ où $m$ est l'indice de l'hypothèse de Riemann). Le problème de savoir si la fonction $x_1,...,x_k \mapsto \frac{1}{Q(x_1,..,x_k)}$ est donc au moins aussi difficile que ladite conjecture.

Mais vous avez aussi une équation diophantienne $Q(x_1,...,x_k)=0$ qui a des solutions si et seulement si la théorie ambiante est contradictoire (i.e. $0=1$ est prouvable)!!! Dans ce cas, si ladite théorie est consistante, l'équation correspondante n'a pas de solution, mais il est alors impossible de prouver ce dernier fait (par le deuxième théorème de Gödel).

Noter que même si COQ n'est pas Turing complet, y entrer des équations diophantiennes et des fonctions polynômiales ne pose aucun problème donc cette problématique ("indécidabilité générale des problèmes d'ensembles de définitions de fonctions pour de simples fractions rationnells à coefficients entiers") le concerne aussi.

Ca ne concerne que les logiciens étriqués tout ça

Non et je suis de plus en plus convaincu que chaque fois qu'un ado confus ou un troll ou quelqu'un de déçu par les maths demande (plusieurs fois par jour sur le net)

Mais au fond peut-on diviser par 0?

C'est ce problème qui se cache derrière: la validité de la construction syntaxique $\frac{T}{0}$ opposée à son inconvenance sémantique (les gens savent qu'ils ne trouveront jamais de nombre $N$ tel que $N \times 0=1$, leur plainte porte sur autre chose), et l'insatisfaction consécutive aux non-réponses qui été présentées au sujet frustré dans le cadre de cette activité bancale qu'est la détermination "d'ensemble de définition" (circonscrite -et pour cause- dans l'enseignement à des situations où l'expression problématique est invariablement un polynôme de petit degré incrusté dans une racine carrée, un log, ou un dénominateur: on est en plein dans l'application chorégraphiée de procédures types impossibles à réutiliser ailleurs).
On pourrait rattraper ça en déclarant qu'en fait c'est l'ensemble de définition d'une expression qui est cherché (et alors ledit ensemble se verrait enfin doté d'une véritable définition précise, par induction sur la taille de l'expression et en se ramenant à ces constituants simples). Or le choix retenu semble avoir été de faire comme si ces choses étaient des propriétés intrinsèques des fonctions, mystérieux "procédés" et là pardon mais on plonge la tête la première dans les pseudo-sciences les plus grasses.

Foys, ne pourrait-on pas définir K de type Set,
P (z: prod K K) := not (K_mult (fst z) (snd z) = 0).
et utiliser P et sig pour définir un nouveau type qui serait le domaine de K_div?
Ca semble plus proche de ce qu'on fait d'habitude en mathématiques. Quels sont les inconvénients d'une telle démarche par rapport à la tienne?

@Alesha: on peut faire ça avec Type, Set n'est pas indispensable.

Le problème n'est pas là, ça risque d'être moins maniable, la fonction division serait alors de la forme Kdiv2: {x:prod K K | P x} -> K, et alors comment définir des fonctions rationnelles comme $x\mapsto \frac{x^2}{x^{-1}+x^{-4}-2}$? Comment les composer? Il faut être en mesure de décider la nullité ou non d'un nombre pour manier Kdiv2 dans les calculs ce qui n'est pas du tout donné pour certains corps (je ne m'y suis jamais intéressé mais je sais que le $\R$ intuitionniste apporte quelques subtilités).