Methodo, 5/11
Résumé de cours (virtuel)
sur les définitions
cours précédent
........ cours
suivant..........tous
les cours
Définir
-
Typer
-
Les expressions mathématiques représentent des nombres,
des énoncés ou des objets plus élaborés (fonctions,
ensembles, ensembles de fonctions, etc). Pour éviter les expressions trop
longues, et pour améliorer la lisibilité de leur discours, les
mathématiciens attribuent des noms en posant des définitions. Une
définition introduit donc un nom, et lui associe un sens. Mais avant de
convenir du sens en question, il est utile de convenir de la nature de l'objet
défini.
Pour classer leurs objets selon leur nature, les physiciens
parlent de dimension, les informaticiens parlent de types, et les
mathématiciens parlent d'ensembles. Typer une notion, c'est indiquer
à quel ensemble elle appartient. Le type d'une notion est en
général fonctionnel, en ce sens que cette notion attend des
arguments de divers types, et rend un résultat d'un certain type.
Par exemple $pair$ attend un entier, et rend une valeur de vérité
($V$ ou $F$). Sans se préoccuper de quelle est cette valeur, on peut
capturer la nature de $pair$ dans la formule $pair: Z ->
B$ qu'on peut lire: "$pair$ est $Z ->
B$".
De la même façon, on dira que l'addition $Plus$
des complexes est de type $C2 ->
C$.
Autre exemple, on peut concevoir "continu" comme attendant une fonction $f:
R -> R$ et un nombre $ a: R$ (et qui rend
$Vrai$ ou $Faux$ selon que $f$ est continue en $a$ ou non). On résume
cette conception en écrivant:
$continu_en: Rx(R -> R) ->B$.
Il y a bien entendu un autre "continu",
$continu_partout: (R -> R) ->B$, qu'il
faut bien distinguer du premier.
On peut aussi envisager un "continu" intermédiaire
$continu_sur:
(P(R)x(R -> R)
->B$,
qui permet de dire que $f$ est continue sur $I$.
Si on veut en plus libéraliser le domaine de définition de $f$,
ça se complique:
on peut commencer par dire que pour chaque $I$, on a un
$continu_pour_I:
(I -> R)
->B$,
qui permet de dire que $f$ définie sur $I$, y
est continue.
On peut alors faire passer le $I$ à droite de $:$, en indiquant son type
((c'est une partie de $R$).
$continu_param:
(I:(P(R))(I -> R)
->B$,
qui remplace avantageusement la multitude des
$continu_pour_I$. Notez que $I$ est libre dans le type de $continu_pour_I$, et
lié dans celui de $continu_param$.
-
Définir
Dans la pratique, on ne définit pas l'objet lui-même:
$constante_surR:= f |-> Ptt x,y:R, f(x)=f(y)$
mais plutôt la construction correspondante:
$f est_constante_sur_R:<=> Ptt x,y:R, f(x)=f(y)$
Cette habitude est à rapprocher de l'habitude qui consiste à
définir $f$ par $f(x)= ...$ au lieu de $f:= x |-> ...$.
Dans une telle définition, il faut donc bien voir les arguments, qui ne
sont pas mis en évidence par les $|->$, et les eventuelles contraintes
qui les lient.
Par exemple on peut poser
$f est_constante_sur J :<=> Ptt x,y:J, f(x)=f(y)$.
Dans cette formulation de la définition, il faut voir que les deux
arguments sont $f$ et $J$, comprendre leur nature et
la contrainte qui les lient, à
savoir que $J$ est
contenu dans le DD de $f$.
Pour lever toute ambiguïté, on pourra dire
"Si $J$ est une partie du DD de $f$, on dira que
$f est_constante_sur J $
si (et seulement si) $Ptt x,y:J, f(x)=f(y)$".
Et si on veut être encore plus explicite sur la nature de $f$, on pourra
dire
"Si $f$ est une fonction de DD quelconque et $J$ est une partie de ce DD, on dira que
$f est_constante_sur J $
si (et seulement si) $Ptt x,y:J, f(x)=f(y)$".
Bien entendu, ça alourdit gravement, c'est pourquoi on
préfère souvent rester elliptique.
cours précédent
........ cours
suivant..........tous
les cours
Andre.HIRSCHOWITZ
Last
modified: Oct 1