Logique D'ordre Supérieur


Logique D'ordre Supérieur

Logique d'ordre supérieur

Les logiques d'ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d'utiliser les variables dans les termes en tant que fonctions, et dans les expressions en tant que prédicats.

D'un point de vue sémantique, cela revient à dire que l'on considère les fonctions et prédicats comme des objets à part entière, au même titre que, par exemple, un nombre entier. On s'autorisera ainsi, d'une part, à quantifier les prédicats et fonctions et, d'autre part, à donner des fonctions ou des prédicats en arguments d'autres fonctions et prédicats. Néanmoins, on pourra se doter d'un système de typage qui restreindra le genre d'objet qui pourra être donné en tant que tel ou tel argument de tel ou tel prédicat ou telle ou telle fonction.

Un prédicat d'ordre supérieur est un prédicat qui prend comme argument un ou plusieurs autres prédicats. De manière générale, un prédicat d'ordre n prend comme argument un ou plusieurs prédicats d'ordre n-1, avec n > 1. Les mêmes définitions s'appliquent aux fonctions d'ordre supérieur.

Les lambda-calculs typés, comme le calcul des constructions, s'inspirent de telles logiques dans ce qu'on appelle le paradigme fonctionnel. Un lien fort est tissé entre les mathématiques et l'informatique grâce à l'isomorphisme de Curry-Howard qui associe un lambda-calcul à une logique. C'est de ce domaine que sont issus les langages de programmation fonctionnelle.

Logique du second ordre

La logique du second ordre étend celle du premier ordre par l'ajout de variables relationnelles, qui peuvent donc être quantifiées. Par exemple, \forall P \, \exists x\, \forall y\, P(x,y) est une formule de la logique du second ordre. En particulier la logique du second ordre permet de quantifier sur des fonctions (vues comme des cas particuliers de relations). L'axiome d'induction est un axiome du second ordre:

(\forall P\in A\to A)\ ((\forall a\in A) \ ((\forall b\in A) P(b)) \Rightarrow P(a)) \quad\Rightarrow \quad (\forall a\in A) P(a).

La logique monadique du second ordre se restreint aux variables fonctionnelles unaires, qui sont en fait les ensembles. Elle permet d'avoir des résultats de décidabilité plus intéressants qu'au premier ordre : par exemple, la théorie monadique d'un ordinal dénombrable est décidable.

Logique du troisième ordre

Elle utilise des objets de troisième type, comme les filtres ou ultrafiltres, mais est rarement mentionnée en tant que telle.

Voir aussi

  • Portail des mathématiques Portail des mathématiques
  • Portail de la logique Portail de la logique
  • Portail de l’informatique Portail de l’informatique
Ce document provient de « Logique d%27ordre sup%C3%A9rieur ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Logique D'ordre Supérieur de Wikipédia en français (auteurs)

Regardez d'autres dictionnaires:

  • Logique d'ordre superieur — Logique d ordre supérieur Les logiques d ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d utiliser les variables dans les termes en tant que fonctions, et dans les expressions en… …   Wikipédia en Français

  • Logique d'ordre supérieur — Les logiques d ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d utiliser les variables dans les termes en tant que fonctions, et dans les expressions en tant que prédicats. D un… …   Wikipédia en Français

  • Logiques d'ordre supérieur — Logique d ordre supérieur Les logiques d ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d utiliser les variables dans les termes en tant que fonctions, et dans les expressions en… …   Wikipédia en Français

  • Fonction D'ordre Supérieur — En mathématiques et en informatique, les fonctions d ordre supérieur ou les fonctionnelles sont des fonctions qui ont au moins une des propriétés suivantes : prendre une ou plusieurs fonctions comme entrée, renvoyer une fonction. En… …   Wikipédia en Français

  • Fonction d'ordre superieur — Fonction d ordre supérieur En mathématiques et en informatique, les fonctions d ordre supérieur ou les fonctionnelles sont des fonctions qui ont au moins une des propriétés suivantes : prendre une ou plusieurs fonctions comme entrée,… …   Wikipédia en Français

  • Fonctions d'ordre supérieur — Fonction d ordre supérieur En mathématiques et en informatique, les fonctions d ordre supérieur ou les fonctionnelles sont des fonctions qui ont au moins une des propriétés suivantes : prendre une ou plusieurs fonctions comme entrée,… …   Wikipédia en Français

  • Fonction d'ordre supérieur — En mathématiques et en informatique, les fonctions d ordre supérieur ou les fonctionnelles sont des fonctions qui ont au moins une des propriétés suivantes : prendre une ou plusieurs fonctions comme entrée, renvoyer une fonction. En… …   Wikipédia en Français

  • ordre — [ ɔrdr ] n. m. • 1080 sens II; lat. ordo, ordinis I ♦ (1155) Relation intelligible entre une pluralité de termes. ⇒ organisation, structure; économie. « L idée de la forme se confond avec l idée de l ordre » (A. Cournot). 1 ♦ Didact. Disposition …   Encyclopédie Universelle

  • LOGIQUE MATHÉMATIQUE — La logique au sens étroit du terme, c’est à dire la logique formelle par opposition à l’épistémologie ou à la théorie de la connaissance, se propose de donner une théorie de l’inférence formellement valide. Elle considère comme valide toute… …   Encyclopédie Universelle

  • Logique Combinatoire — Pour les articles homonymes, voir combinatoire (homonymie). Avertissement: Cet article traite de la logique combinatoire, au sens qu a ce mot en logique mathématique et en informatique théorique. Il ne doit pas être confondu avec ce que l on… …   Wikipédia en Français