Lazi

Nommage des mathématiques lazi

Contexte

Il y a un problème dans le nommage actuel entre la doc et le code. Il est nécessaire de corriger ça et de revoir le nommage.
Voir la page "Conventions de nommage".

Question

Comment nommer les différentes mathématiques lazi.

Étude

Le nommage dans les sources

Définition de la fondation en lazi

lazi1 pour le second niveau. Le premier niveau n'est pas écrit en lazi.
Puis pour les extensions lazi1_E4 etc

Dans les testes de validation

Pareil que dans les sources

Dans lazi-compute

Qu'une seule mention :

PFormula Formula::simplify_to_Lazi1()
{
  PFormula f(this);
  while(f->is_notation())
    f=f->simplify();
  return f;
}

Dans "lazi-translate"

-- | Define Lazi0aFm data type and functions for this type. Lazi0aFm is the type of lazi.0.0 formula (just apply and keywords).
Dans les testes de "lazi-translate"
data Format = FormatXML | 
               FormatSources | 
               FormatComputeFm | -- Like Sources, but without notations, just basic ComputeFm
               FormatLazi0a | -- Lazi.0.0 : just keywords & applications
               FormatLazi0aDepth | -- same as FormatLazi0a, used to print just the depths of formulas.
               FormatNotDef deriving Eq
-- Convert a Sources in a lazi1 formula sources.
sourcesToLazi1 :: String -> Sources -> Sources
sourcesToLazi1 name s = [ SourceDefFunc $ Definition name $
    Dict [
      (
        "defs",
        Dict $ map (\(Definition name val)-> (name,FormulaRepr val)) (getDefinitions s)
      )]
  ]
-- Do we have to translate all the includes in a XMLDefs/XML Lazi1 file (all defs in one 1-formulas in a structure)?
                    if not (null $ optOutputLazi1 opts) 
                    then
                      writeFileOrStd (optOutput opts) $ definitionsToComputeFmTxt $ getDefinitions $ sourcesToLazi1 (optOutputLazi1 opts) s

lazi1... est beaucoup moins fréquent que lazi0...

Dans le front-en "lazi"

--input0 FILE : a source file to read 
--inputs1 and --input1 : Optional. Same as without the "1", but it's for lazi1 definitions. See also --lazi1.
--lazi1 DEFNAME (default "$lazi1_def_name") : name to use to define the lazi1 definitions.

# Output Lazi0 definition xml file

my @input_files0=(); # List of files containing lazi0 definitions. ('--inputs0')

my @input_files1=(); # List of files containing lazi1 definitions.('--input1')

Le nommage dans les docs

Dans le wiki

Lazi.0 désigne la fondation mathématique Lazi.
lazi.0.a désigne la fondation sans notation avec juste les 6 règles de calcul et la règle de la preuve.
Lazi.0.b désigne lazi.0.0 plus les diverses notations telles que :

  • les noms définis
  • les fonctions
Lazi.0.c désigne lazi.0.b plus les deux règles de déduction :
  • induction
  • tiers exclu.
lazi.0.d désigne lazi.0.c avec la règle de déduction d'extension.
lazi.1 définie un groupe d'extension permetant la généralisation classique des preuves: quantificateurs, implication etc.

Éléments à prendre en compte

Liberté de syntaxe suivant les langages.

Il faut pouvoir spécifier : la dernière mathématique définie, la première, la famille de mathématique.

Donner des noms, des numéros, les deux ?

Quand changer de numéro majeur ?

Réponse

Le nommage

Une mathématique lazi est désigné par lazi.nom1.nom2....
ou nomn peut être un nom alphanumérie ou un nombre, sans caractère spéciaux (par exemple pas de "_" ou "-").

lazi.nom1....nomk* désigne l'ensemble des mathématiques sous lazi.nom1....nomk.

Quand lazi.nom1....nomk+1 existe et que les mathématiques lazi.nom1....nomk.* sont imbriquées alors lazi.nom1....nomk désigne la plus grande extension mathématique de lazi.nom1....nomk.*

Le nommage quand le point n'est pas accepté

On remplace le point par "_". Donc par exemple lazi_1_3

lazi.0.*

lazi.0.0 : pas de notation, les 6 règles de base
lazi.0.1 : avec les notations et les 6 règles de base
lazi.0.2 : avec les notations et toutes les règles (les 7).

lazi.1.*

lazi.1.0 : la mathématique définie par la fondation.

@todo