Évaluation et dérivation d'expressions arithmétiques

Syntaxe abstraite

Utiliser MPS pour définir le métamodèle d'un langage permettant de définir des expressions arithmétiques composées de :

• constantes
• variables
• addition, soustraction, produit et quotient
• mise entre parenthèse

La structure du métamodèle correspondra à :

• rootExpression, pour associer un nom à une expression : e1 = 3 * (x + 2)
• expression, concept abstrait dont héritent les autres
• value, pour une valeur numérique
• varref, pour l'utilisation d'une variable
• parenthesized, pour une expression entre parenthèses
• binop, concept abstrait pour les quatre opérateurs binaires
• sum, pour la somme de deux expressions
• difference, pour la différence de deux expressions
• product, pour le produit de deux expressions
• quotient, pour le quatient de deux expressions

Syntaxe concrète

Ajouter un aspect editor aux concepts concrets pour disposer d'un éditeur d'expressions dans MPS

Sémantique

Définir une théorie dans Isabelle pour l'évaluation et la dérivation d'expressions. Le listing ci-dessous peut vous servir de point de départ.

Transformation depuis un modèle MPS vers Isabelle

Ajouter aux concepts du métamodèle MPS un aspect textGen afin de transformer une rootExpression en une abbreviation pour votre theorie. Par exemple : e1 = 2 * x + 3 sera transformé en

Quelques preuves de théorèmes

Commencez par prouver que {$\frac{\partial}{\partial x}2x = 2$} Il vous faudra ajouter des axiomes de simplification pour cela.

Essayez ensuite de démontrer que {$\frac{\partial}{\partial x}ax+b = a$}

Pour finir, démontrez que {$\frac{\partial}{\partial x}axx = 2ax$}

ancien sujet