Programmation logique
La programmation logique est un type de paradigme de programmation qui est en grande partie basée sur la logique formelle. Tout programme écrit dans un langage de programmation logique est un ensemble de phrases s sous forme logique, exprimant des faits et des règles concernant un domaine problématique.
Les principales familles de langages de programmation logique comprennent Prolog, la programmation d’ensembles de réponses (ASP) et Datalog. Dans toutes ces langues, les règles sont écrites sous la forme de clauses :
H : - B 1,…, B n.
et sont lus déclarativement comme des implications logiques:
H si B 1 et… et B n.
H est appelé le chef de la règle et B 1,..., B n est appelé le corps. Les faits sont des règles qui n'ont pas de corps et qui sont écrites sous la forme simplifiée:
H.
Dans le cas le plus simple où H, B 1,..., B n sont toutes des formules atomiques, ces clauses sont appelées clauses définies ou clauses de Horn. Cependant, il existe de nombreuses extensions de ce cas simple, le plus important étant le cas dans lequel les conditions dans le corps d'une clause peuvent également être des négations de formules atomiques. Les langages de programmation logique qui incluent cette extension ont les capacités de représentation des connaissances d'une logique non monotone.
En ASP et Datalog, les programmes logiques n’ont qu’une lecture déclarative et leur exécution est effectuée au moyen d’une procédure d’épreuve ou d’un générateur de modèle dont le comportement n’est pas censé être sous le contrôle du programmeur. Cependant, dans la famille de langues Prolog, les programmes logiques ont également une interprétation procédurale en tant que procédures de réduction d'objectifs:
pour résoudre H, résoudre B 1, et... et résoudre B n.
Considérons, par exemple, la clause suivante:
faillible (X) : - humain (X).
basé sur un exemple utilisé par Terry Winograd pour illustrer le planificateur de langage de programmation. Comme une clause dans un lo programme gic, il peut être utilisé à la fois comme une procédure pour vérifier si X est faillible en testant si X est humaine, et comme une procédure pour trouver un X qui est faillible en trouvant un X qui est humain. Même les faits ont une interprétation procédurale.
Prenons, par exemple, la clause suivante:
humain (socrate).
peut être utilisé à la fois comme une procédure pour montrer que socrate est humaine, et comme une procédure pour trouver un X qui est humain par « assignant » socrate à X.
La lecture déclarative de programmes logiques peut être utilisée par un programmeur pour vérifier son exactitude.
De plus, les techniques de transformation de programme basées sur la logique peuvent également être utilisées pour transformer des programmes logiques en des programmes logiquement équivalents et plus efficaces. Dans la famille de langages de programmation logique Prolog, le programmeur peut également utiliser le comportement connu du mécanisme d’exécution pour résoudre les problèmes afin d’améliorer l’efficacité des programmes.
