/* ----------------------------------------------------------------------
   $Id: specifications.txt 27 2006-10-27 08:24:41Z masterli2 $

   Nom          : specifications.txt
   Type         : texte
   Contenu      : spécification des modules à réaliser pour ptq
   Commentaires : Même si ça n'est pas recommandé par les canons du
                  génie logiciel, ces spécifications sont très
                  dynamiques : c'est aussi ici que peuvent avoir lieu
                  les éventuelles discussions. 
   
---------------------------------------------------------------------- */

* Pré-traitement du lexique : 

  Idée : il faudrait pouvoir disposer d'un lexique (et d'une tds) dans
  un fichier externe, qu'on puisse modifier et recharger
  dynamiquement, sans exclure la méthode actuelle d'ajout de lexemes
  ou d'identificateurs on line. 

  Mais la lecture du fichier lexique demande un parsage de la
  lamnda-expression associée : il faut donc passer par
  lex/yacc. L'idéal serait donc qu'au cours d'un "parse", on puisse
  demander à yacc d'ouvrir un autre fichier pour appliquer sa
  grammaire dessus. Malheureusement, je ne suis pas sûr que ce soit
  possible avec yacc...

  Une autre option est de prévoir la possibilité d'enregistrer le
  lexique et la tds courants (ie en mémoire) dans un fichier,
  structuré de telle façon qu'il pourrait être ensuite rechargé par le
  programme sans nécessiter de parsage. On peut même imaginer que ce
  fichier soit dans un format d'échange connu, par exemple XML (qui
  permet de représenter des arbres...)


* Evaluation des formules/phrases dans un modèle : 

  Idée : permettre que certaines phrases assertives (jean dort) soient
  vues comme modifiant le modèle (au sens tarskien), et que l'on
  puisse alors poser des questions sur le modèle (est-ce que tous les
  hommes dorment ?), dont la réponse est donnée par une évaluation de
  la formule correspondant à la phrase dans le modèle courant.

  Module fortement inspiré par le travail réalisé en M1 l'an dernier. 

* Introduction du typage (e,t...) dans le système : 

  Idée : permettre une expression plus générale de la règle de
  combinaison des lambda-expressions : plutôt que de fixer dans chaque
  règle le foncteur et l'argument, on n'aura plus qu'a dire :
  "si le constituant X est de type a, si le constituant Y est de type
  <a, b>, alors appliquer Y à X. 

  Dès lors, on peut aussi envisager des stratégies de montée de type
  déclenchées lorsque les types ne sont pas compatibles.

* Benchmark : plate-forme de test

  Idée : faire en sorte que l'on puisse tester de façon systèmatique
  (et automatique) les résultats du système : il faut prévoir la liste
  des inputs testés, et la liste des outputs attendus, et être capable
  de comparer les deux. 

  L'idée est de vérifier la monotonie du système : lors d'un ajout, on
  doit pouvoir vérifier simplement que l'ajout n'a rien modifié dans
  les résultats déjà stabilisés produit par le système.

  Attention : une telle plate-forme est hautement dynamique (les
  formats de sortie changent souvent).

* Beta-reduction avec résolution du problème de capture de variable

  Idée : apporter une solution propre au problème de la capture des
  variables.

  Plusieurs solutions : 
    - à la prolog : les espaces de noms sont locaux, ou, en d'autres
      termes, toute expression utilise des variables nouvelles
    - par alpha-transformation dès que c'est utile : il faut définir
      dynamiquement l'ensemble des var. libres et l'en des var. liées
      dans une formule, et renommer en cas de conflit.
      Cela nécessite une réflexion sur la stratégie de beta-réduction,
      et une stratégie de renommage

* Reprise d'erreur

  Idée : rendre l'interaction avec le système plus confortable en
  traitant les erreurs de syntaxe simples, avec les méthodes proposées
  dans lex/yacc. (error recovery)

* Interface graphique

  - en sortie : passer par latex, ou par html, pour produire des
    formules plus lisibles ;
  - en entrée : whatever