Lean-14 — Dérivées symboliques de Brzozowski : la finitude qui garantit le matching linéaire

Série SymbolicAI/Lean — Pont vers l’Epic #2978 (le Sudoku comme regex symbolique), livrable C (Lean). See #2978 (partial), See #2162 (homonymie Conway).

Note d’homonymie posée d’entrée. Le héros de notre Epic Lean conway_lean (#2162) est John Horton Conway, mathématicien, créateur du Game of Life. Le célèbre sudoku en regex Perl (Perlmonks, 2002) est l’œuvre de Damian Conway, linguiste-informaticien. Deux Conway distincts. Les deux se « rencontrent » dans cette série : l’un par la reconnaissance par regex, l’autre par la formalisation du Jeu de la Vie. Ce notebook documente ce clin d’œil, pas une confusion.

1. Le problème : pourquoi un reconnaisseur regex devrait être linéaire

Un reconnaisseur d’expressions régulières (regex matcher) lit un mot caractère par caractère. Deux familles :

  • Backtracking (PCRE, moteurs « NFA traditionnels ») : en cas d’échec, le moteur revient en arrière et essaie une autre branche. Simple à implémenter, mais la complexité peut devenir exponentielle (catastrophic backtracking). C’est la famille du sudoku en regex de Damian Conway — un monstre de lookaheads gigantesques.
  • Non-backtracking (DFA / dérivées) : on consomme chaque caractère une seule fois, sans retour. Complexité linéaire en la longueur du mot. C’est la famille de .NET RegexOptions.NonBacktracking (Moseley, Nishio, Rodriguez, Saarikivi, Toub, Veanes, Wan, Xu — Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics, PLDI 2023), de RE# (POPL 2025) et de SymPy.

La question de fond : comment garantir qu’un reconnaisseur non-backtracking termine ? Réponse : si l’ensemble des « états » qu’il peut visiter est fini. Et cet ensemble d’états, c’est exactement l’ensemble des dérivées de la regex — un concept dû à Janusz Brzozowski en 1964.

2. La dérivée de Brzozowski (1964)

Soit une regex \(r\) et un caractère \(a\). La dérivée \(D_a(r)\) est la regex qui reconnaît exactement les mots \(w\) tels que le mot \(a{\cdot}w\) est reconnu par \(r\) :

\[L(D_a(r)) = \{\, w \mid a{\cdot}w \in L(r) \,\}\]

Intuition : « j’ai lu \(a\), que me reste-t-il à reconnaître ? » La définition est récursive sur la structure de \(r\) :

\(r\) \(D_a(r)\)
\(\emptyset\) \(\emptyset\)
\(\varepsilon\) \(\emptyset\)
\(b\) (un caractère) \(\varepsilon\) si \(a = b\), sinon \(\emptyset\)
\(r{\cdot}s\) \(D_a(r){\cdot}s \;\cup\; (\varepsilon \in L(r) ? D_a(s) : \emptyset)\)
\(r \cup s\) \(D_a(r) \cup D_a(s)\)
\(r^*\) \(D_a(r){\cdot}r^*\)

Le matching non-backtracking s’écrit alors trivialement : un mot \(w = a_1 a_2 \dots a_n\) est reconnu par \(r\) ssi la dérivée itérée \(D_{a_n}(\dots D_{a_1}(r)\dots)\) est nullable (reconnaît le mot vide \(\varepsilon\)). On lit chaque caractère une seule fois, en avant.

3. Le théorème de finitude — le résultat qui garantit la terminaison

Théorème (Brzozowski, 1964). L’ensemble des dérivées itérées \(\{D_w(r) \mid w \in \Sigma^*\}\) d’une expression régulière \(r\) est fini — modulo l’équivalence ACI (Associativité, Commutativité, Idempotence) des unions.

C’est ce théorème qui transforme la dérivée d’un concept élégant en un algorithme qui termine : comme l’espace des dérivées est fini, un reconnaisseur qui passe d’une dérivée à la suivante ne peut visiter qu’un nombre borné d’états distincts. D’où la complexité linéaire des moteurs RE# et .NonBacktracking.

Ci-dessous, nous illustrons ce concept sur un mini-projet Lean autonome (sans dépendance Mathlib).

import subprocess
from pathlib import Path

# Le mini-projet Lake no-Mathlib (autonome, a cote des autres projets Lean de la serie).
# Le chemin est calcule depuis le chemin du notebook (resolve du parent) pour pas a voir
# besoin de coder en dur le drive Windows (D: -> /mnt/d/...).
def wsl(cmd, timeout=180):
    # Execute une commande bash dans WSL Ubuntu.
    full = ['wsl', '-d', 'Ubuntu', '--', 'bash', '-lc', cmd]
    try:
        r = subprocess.run(full, capture_output=True, text=True, timeout=timeout)
        return r.returncode, r.stdout, r.stderr
    except subprocess.TimeoutExpired:
        return -1, '', f'TIMEOUT after {timeout}s'

# Tell c.28 strict fondateur (c.30 #18805) : chemin code en dur = MACHINE_PATH leak.
# On utilise le chemin du module (notebook) pour calculer LEAN_PROJECT.
# Path(__file__) ne marche pas pour un .ipynb execute via nbconvert, donc on se rabat
# sur Path.cwd() qui doit etre le cwd du notebook au moment de l'execution.
_nb_dir = Path.cwd().resolve()  # cwd du kernel = dossier symbolique Lean/
_drive = _nb_dir.drive.rstrip(':').lower()
_path_tail = str(_nb_dir).replace(_nb_dir.drive, '').replace('\\', '/').lstrip('/')
# _path_tail = 'dev/CoursIA-18329-trancheB/MyIA.AI.Notebooks/SymbolicAI/Lean'
LEAN_PROJECT = f'/mnt/{_drive}/{_path_tail}/finiteness_lean'

rc, out, err = wsl(f'cat {LEAN_PROJECT}/lean-toolchain')
print('Toolchain:', out.strip())
print('WSL bridge: OK')
Toolchain: leanprover/lean4:v4.33.0
WSL bridge: OK
# Construction du mini-projet Lean (no-Mathlib : rapide, ~10s)
rc, out, err = wsl(f'cd {LEAN_PROJECT} && lake build Finiteness 2>&1')
print(out)
if rc != 0:
    print('STDERR:', err)
print(f'\n[exit={rc}]  Build complet du projet Finiteness (inductive Regex + deriv + exemples).')
ℹ [2/4] Built Finiteness.Basic (4.3s)
info: Finiteness/Basic.lean:99:0: true
info: Finiteness/Basic.lean:100:0: false
info: Finiteness/Basic.lean:106:0: true
info: Finiteness/Basic.lean:107:0: false
info: Finiteness/Basic.lean:108:0: false
ℹ [3/4] Built Finiteness.Basic_en (4.3s)
info: Finiteness/Basic_en.lean:107:0: true
info: Finiteness/Basic_en.lean:108:0: false
info: Finiteness/Basic_en.lean:114:0: true
info: Finiteness/Basic_en.lean:115:0: false
info: Finiteness/Basic_en.lean:116:0: false
Build completed successfully (4 jobs).


[exit=0]  Build complet du projet Finiteness (inductive Regex + deriv + exemples).
# Le source Lean original (concept public de Brzozowski 1964 -- PAS le code d'ezhuchko)
rc, out, err = wsl(f'cat {LEAN_PROJECT}/Finiteness/Basic.lean')
print(out)
/-! # Dérivées symboliques de Brzozowski — démonstration pédagogique autonome

Soit une expression régulière `r` sur un alphabet `α`. La **dérivée** de `r`
par un caractère `a` (Janusz Brzozowski, *Derivatives of Regular Expressions*,
JACM 1964) est l'expression `D_a(r)` qui reconnaît exactement les mots `w` tels
que le mot `a :: w` est reconnu par `r`. Itérée sur les caractères d'un mot, la
dérivée calcule la correspondance (*matching*) **sans reculer**
(non-backtracking) : un mot `w` est reconnu par `r` si et seulement si la
dérivée de `r` par `w` est *nullable* (reconnaît le mot vide ε).

## Le théorème de finitude

Brzozowski (1964) démontre que l'ensemble des dérivées itérées d'une expression
régulière est **fini** — modulo l'équivalence ACI (Associativité, Commutativité,
Idempotence) des unions. C'est cette finitude qui garantit la **terminaison** et
la complexité **linéaire** des reconnaisseurs modernes :
  * .NET `RegexOptions.NonBacktracking` (PLDI 2023),
  * **RE#** (POPL 2025, Varatalu/Veanes/Ernits),
  * SymPy.

## La formalisation Lean constructive (ITP 2025)

La formalisation **constructive** complète en Lean 4 — on construit un ensemble
fini majorant l'espace des dérivées (modulo équivalence) — est due à **Ekaterina
Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner** (*Finiteness of
Symbolic Derivatives in Lean*, ITP 2025), dépôt
[`ezhuchko/finiteness-derivatives`](https://github.com/ezhuchko/finiteness-derivatives).
Sa licence amont n'étant pas confirmée, **ce fichier ne vendore pas leur code** :
il en illustre l'intuition par des définitions et exemples **originaux**, sans
dépendance (pas de Mathlib). Le notebook
[`Lean-14-Finiteness-Derivatives.ipynb`](../../Lean-14-Finiteness-Derivatives.ipynb)
développe la présentation pédagogique et le pont vers l'epic Conway #2162. -/


/-- Une expression régulière minimale sur l'alphabet `α`.
    * `empty` : langage vide ∅
    * `eps`   : langage du mot vide {ε}
    * `char a`: singleton {a}
    * `concat r s` : concaténation r·s
    * `union r s`  : union r ∪ s
    * `star r`     : étoile de Kleene r* -/
inductive Regex (α : Type) where
  | empty : Regex α
  | eps   : Regex α
  | char  : α → Regex α
  | concat : Regex α → Regex α → Regex α
  | union  : Regex α → Regex α → Regex α
  | star   : Regex α → Regex α
  deriving Repr

open Regex

/-- `nullable r` : la regex `r` reconnaît-elle le mot vide ε ?
    (Point fixe de la reconnaissance : une dérivée nullable ⇒ le mot lu est
    accepté.) -/
def nullable {α : Type} : Regex α → Bool
  | empty => false
  | eps => true
  | char _ => false
  | concat r s => nullable r && nullable s
  | union r s => nullable r || nullable s
  | star _ => true

/-- La **dérivée de Brzozowski** `D_a(r)` : reconnaît les mots `w` tels que
    `a :: w ∈ L(r)`. Définition récursive standard ; le cas `concat` fait
    apparaître une union quand le facteur gauche est nullable — c'est cette
    union qui, modulo ACI, borne l'espace des dérivées. -/
def deriv {α : Type} [BEq α] (a : α) : Regex α → Regex α
  | empty => empty
  | eps => empty
  | char b => if a == b then eps else empty
  | concat r s => if nullable r then union (concat (deriv a r) s) (deriv a s)
                  else concat (deriv a r) s
  | union r s => union (deriv a r) (deriv a s)
  | star r => concat (deriv a r) (star r)

/-- Dérivée par un mot (liste de caractères) : pliée de gauche à droite. -/
def derivWord {α : Type} [BEq α] (w : List α) (r : Regex α) : Regex α :=
  w.foldl (fun r' c => deriv c r') r

/-- Un mot `w` est reconnu par `r` ssi sa dérivée est nullable. C'est le
    *matching* non-backtracking : on consomme chaque caractère une seule fois,
    sans retour en arrière. (`matches` est un mot réservé en Lean 4, d'où le
    nom `accepts`.) -/
def accepts {α : Type} [BEq α] (w : List α) (r : Regex α) : Bool :=
  nullable (derivWord w r)

/-! ## Exemples : la finitude en action

On observe sur des exemples concrets que l'espace des dérivées reste fini (et
souvent minuscule) — c'est précisément le théorème de Brzozowski. -/

/-- Le langage `a*` (étoile sur le caractère 'a'). -/
def aStar : Regex Char := star (char 'a')

/- `a*` est un **point fixe** de sa dérivée par 'a' : `D_a(a*) ≡ a*`.
   L'espace des dérivées est donc réduit à un singleton — d'où la reconnaissance
   en temps linéaire. -/
#eval accepts ['a', 'a', 'a', 'a'] aStar   -- "aaaa" ∈ a*  → true
#eval accepts ['a', 'b'] aStar              -- "ab"  ∉ a*  → false

/-- Le langage `ab` (le mot "ab"). Les dérivées successives par les préfixes
    forment l'ensemble fini {ab, b, ε, ∅}. -/
def abWord : Regex Char := concat (char 'a') (char 'b')

#eval accepts ['a', 'b'] abWord   -- "ab" ∈ ab → true
#eval accepts ['a'] abWord        -- "a"  ∉ ab → false
#eval accepts ['a', 'b', 'c'] abWord -- "abc" ∉ ab → false

/- Dérivée concrète : `D_a(char a) = ε` (le singleton est « consommé »). -/
example : deriv 'a' (char 'a') = eps := by
  simp [deriv]

/- Dérivée concrète : `D_b(char a) = ∅` (caractères distincts). -/
example : deriv 'b' (char 'a') = empty := by
  simp [deriv]

/-! ## Note d'homonymie (footnote pédagogique)

Le pont vers l'Epic Conway #2162 appelle une clarification : **Damian Conway**
(auteur du célèbre *sudoku en regex Perl*, Perlmonks 2002) n'est pas **John
Horton Conway** (mathématicien, créateur du *Game of Life* — le héros de notre
Epic Lean `conway_lean`). Les deux Conway « se rencontrent » dans cette série
SymbolicAI/Lean : l'un par la reconnaissance par regex, l'autre par la
formalisation du Jeu de la Vie. Clin d'œil à documenter, pas une confusion. -/

Lecture des sorties

Les #eval du fichier compilent et s’exécutent (capturées dans la sortie lake build ci-dessus) :

  • accepts ['a','a','a','a'] aStar → true : le mot “aaaa” appartient a a* (l’étoile reconnaît toute répétition de ‘a’).
  • accepts ['a','b'] aStar → false : “ab” n’appartient pas a a* (le ‘b’ casse la répétition).
  • accepts ['a','b'] abWord → true, accepts ['a'] abWord → false, accepts ['a','b','c'] abWord → false : le mot “ab” et lui seul.

Ces résultats sont obtenus par dérivation itérée + test de nullabilité — la définition même du matching non-backtracking. Les deux example (deriv 'a' (char 'a') = eps, deriv 'b' (char 'a') = empty) sont prouvés par simp [deriv] : on consomme un caractère singleton, ou on échoue.

4. Le point fixe — pourquoi l’espace des dérivées est minuscule

Considérez r = a* (l’étoile sur le caractère ‘a’). Calculons sa dérivée par ‘a’ :

\[D_a(a^*) = D_a(a){\cdot}a^* = \varepsilon{\cdot}a^* \equiv a^*\]

La dérivée de a* par ‘a’ est a* elle-même : c’est un point fixe. L’espace des dérivées de a* est donc réduit au **singleton {a*}**. Le reconnaisseur n’a qu’un seul état a visiter — d’où une reconnaissance en temps strictement linéaire, sans aucune structure de données auxiliaire.

C’est cette propriété — finitude de l’espace des dérivées — que Brzozowski (1964) a démontrée en général, et qui sous-tend tous les moteurs linéaires modernes.

5. La formalisation Lean constructive — Zhuchko, Maarand, Veanes, Ebner (ITP 2025)

La formalisation complète en Lean 4 du théorème de finitude est due a Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner :

E. Zhuchko, H. Maarand, M. Veanes, G. Ebner. Finiteness of Symbolic Derivatives in Lean. ITP 2025. Dépôt : ezhuchko/finiteness-derivatives.

La preuve est constructive : étant donnée une expression \(R\), on construit un ensemble fini qui surestime (modulo l’équivalence des dérivées) l’ensemble des dérivées de \(R\). Elle réutilise l’infrastructure de formalisation des expressions régulières en Lean 4, illustrant la réutilisabilité du cadre.

⚠️ Licence amont non confirmée. Conformément a l’issue #2978, ce notebook ne vendore pas le code d’ezhuchko. Le mini-projet finiteness_lean/ ci-dessus est entièrement original : il illustre le concept public de Brzozowski (1964) par des définitions et exemples écrits spécifiquement pour cette série pédagogique, sans aucune dépendance (Mathlib exclu). Toute réutilisation du dépôt ezhuchko/finiteness-derivatives est subordonnée a la confirmation de sa licence.

Companion : CPP 2024 (extended regex matching with lookarounds, Zhuchko/Veanes/Ebner) — même lignée de recherche.

5b. Où se situe la finitude dans le programme « automates symboliques »

Le théorème de finitude de ce notebook n’est pas isolé : c’est une brique d’un programme de recherche plus vaste, celui des automates symboliques (SFA), programme développé par Margus Veanes et ses co-auteurs (notamment Veanes, Bjørner, Nachmanson et Bereg, CAV 2014 — Monadic Decomposition ; D’Antoni et Veanes, POPL 2014 — Minimization of Symbolic Automata). Un SFA est un automate dont les transitions portent non pas des caractères mais des prédicats d’une algèbre de Boole effective - ce qui permet de traiter de grands alphabets (Unicode) sans les énumérer. À noter : Margus Veanes figurait parmi les participants au Dagstuhl Seminar 17142 (avril 2017, Formal Methods of Transformations, organisé par Filiot/Maneth/Seidl), mais ce séminaire portait sur les transducteurs et non sur les SFA.

Trois résultats de ce programme se répondent, et la finitude des dérivées en est le socle côté reconnaissance :

Brique du programme Ce qu’elle garantit Rapport a ce notebook
Finitude des dérivées (Brzozowski ; ce notebook, ITP 2025) l’ensemble des dérivées est fini -> reconnaisseur a nombre fini d’états le cœur du notebook
Minimisation symbolique (D’Antoni & Veanes, POPL’14) compresse ce reconnaisseur en son minimal borne la taille après construction
Décomposition monadique (Veanes et al., CAV’14) quand une contrainte multi-variable s’éclate en prédicats mono-variable gouverne l’émission côté resolution (cf Sudoku-13 section 6b)

Le même fil, trois notebooks. La finitude (Prouver, ici) garantit que la reconnaissance non-backtracking de RE# (Vérifier) termine en temps linéaire ; la décomposition monadique décide quand Z3 (Résoudre) atterrit la grille sans saturer. Les mêmes auteurs (Veanes, Ebner) signent la formalisation Lean et la théorie des automates symboliques : la preuve de ce notebook et le moteur du Sudoku-13 sont deux faces d’un seul programme.

6. Le pont vers l’Epic Conway #2162

Ce notebook est le troisième pilier du triptyque #2978 :

Pilier Outil Rôle
Résoudre (produire une grille) Z3 (lignée Rex / RegexToSMT) Le résolveur — génère un témoin
Vérifier (valider une grille) RE# / .NonBacktracking Le vérificateur — reconnaissance en temps linéaire
Prouver (garantir la terminaison) Lean — dérivées de Brzozowski Ce notebook — la finitude sous-jacente

Les trois opérations distinctes du paysage regex symbolique : résoudre ≠ vérifier ≠ prouver. La reconnaissance non-backtracking de RE# est la finitude des dérivées, rendue algorithmique.

Et le clin d’œil final : le héros de notre Epic Lean conway_lean — la formalisation du Game of Life de John Horton Conway — « croise » ici le sudoku en regex de Damian Conway. Deux Conway, deux génies, une même série SymbolicAI/Lean.

Voir conway_lean (Epic #2162, preuve de correction Hashlife) et le notebook Lean-16a-Conway-Man-and-Work.

Exercices

Cette section compte deux familles d’exercices. Les trois exercices Lean ci-dessous se complètent dans le fichier Finiteness/Basic.lean du mini-projet, puis se valident par lake build Finiteness (cellule ci-dessus). Les trois exercices Python qui les suivent (nullable, derivative, matches) se résolvent directement dans leurs cellules : ils ne passent ni par Basic.lean ni par lake build, et se vérifient par les tests commentés dans chaque énoncé.

Exercice 1 (dérivée). Ajoutez un constructeur Regex.plus : Regex α → Regex α (le langage \(r^+\) = une occurrence ou plus). Définissez son cas dans nullable et dans deriv. Indice : \(r^+ = r{\cdot}r^*\), donc \(D_a(r^+) = D_a(r){\cdot}r^*\).

-- TODO étudiant : constructor + nullable case + deriv case
-- def nullable ... | plus r => ...
-- def deriv   ... | plus r => ...

Exercice 2 (reconnaissance). Construisez la regex du langage « les mots sur {a,b} contenant au moins un ‘a’ », puis vérifiez par #eval accepts que “ba” est reconnu mais “bb” ne l’est pas. Indice : (a∪b)* · a · (a∪b)*.

-- TODO étudiant
-- def hasA : Regex Char := ...
-- #eval accepts ['b','a'] hasA   -- attendu : true
-- #eval accepts ['b','b'] hasA   -- attendu : false

Exercice 3 (finitude explicite). Montrez par le calcul (une série de #eval de deriv itérés) que l’espace des dérivées de concat (char 'a') (char 'b') est bien fini : partez de abWord, dérivez par ‘a’, puis par ‘b’, et observez que la dérivée finale est nullable (eps) puis devient empty si on dérive encore. Indice : #eval deriv 'a' abWord, #eval deriv 'b' (deriv 'a' abWord).

Exercice 1 — nullable : une regex reconnaît-elle le mot vide ?

Une regex est représentée par un tuple imbriqué (convention partagée par les 3 exercices ci-dessous) :

('#empty',)              # ∅  : langage vide
('#eps',)                # ε  : le mot vide seulement
('#char', c)             # un seul caractère c
('#concat', r1, r2)      # r1 · r2
('#union', r1, r2)       # r1 + r2
('#star', r)             # r* (zero, une ou plusieurs occurrences)
('#plus', r)             # r+ = r · r*  (une ou plusieurs ; miroir de l'Ex.1 Lean)

Une regex \(r\) est nullable si \(\varepsilon \in L(r)\) (elle accepte le mot vide). C’est la brique de base dont la dérivée (Ex. 2) et la reconnaissance (Ex. 3) ont besoin.

Objectif. Écrire nullable(r) retournant True ssi \(\varepsilon \in L(r)\).

Indice. eps → True ; empty / char → False ; concat → ET des deux ; union → OU des deux ; star → toujours True ; plus → comme son sous-terme.

Étapes. (1) Filtrer (match) sur la tête du tuple pour distinguer les 7 cas ; (2) pour concat/union/plus, récursion sur le(s) sous-terme(s).

def nullable(r):
    # TODO etudiant : True ssi la regex r accepte le mot vide.
    # Indice : 'eps'->True ; 'empty'/'char'->False ; 'star'->True ;
    #          'concat'->nullable(r1) and nullable(r2) ;
    #          'union' ->nullable(r1) or  nullable(r2) ; 'plus'->nullable(r1).
    # Etape 1 : match sur r[0] pour distinguer les 7 cas.
    # Etape 2 : recursion sur les sous-termes pour concat/union/plus.
    return None

# Tests (a decommenter) :
# assert nullable(('#eps',)) is True
# assert nullable(('#empty',)) is False
# assert nullable(('#char', 'a')) is False
# assert nullable(('#concat', ('#char', 'a'), ('#eps',))) is False
# assert nullable(('#union', ('#char', 'a'), ('#eps',))) is True
# assert nullable(('#star', ('#char', 'a'))) is True
# assert nullable(('#plus', ('#char', 'a'))) is False
# print('Exercice 1 : OK')

Exercice 2 — derivative : la dérivée de Brzozowski

La dérivée \(D_a(r)\) est le langage des suffixes : \(w \in D_a(r) \iff aw \in L(r)\). C’est l’opération dont la finitude (théorème central de ce notebook) garantit la terminaison de la reconnaissance.

Objectif. Écrire derivative(r, a) retournant la dérivée de r par le caractère a (convention AST de l’Exercice 1). On renvoie la forme non simplifiée (la simplification est un autre sujet).

Indice. char c → #eps si c == a sinon #empty ; union → dérivée des deux branches ; star r → #concat(derivative(r, a), #star r) ; concat r1 r2 → si nullable(r1) : #union(#concat(D(r1), r2), D(r2)), sinon #concat(D(r1), r2).

Étapes. (1) empty/eps/char (cas de base) ; (2) union/star/plus (une récursion directe) ; (3) concat (test nullable + double branche).

def derivative(r, a):
    # TODO etudiant : derivée de Brzozowski de r par le caractere a (forme non simplifiee).
    # Indice : 'char c' -> '#eps' si c==a sinon '#empty' ; 'eps'/'empty' -> '#empty' ;
                        # Etape 1 : empty/eps/char. Etape 2 : union/star/plus. Etape 3 : concat.
    return None

# Tests (a decommenter) :
# assert derivative(('#char', 'a'), 'a') == ('#eps',)
# assert derivative(('#char', 'a'), 'b') == ('#empty',)
# assert derivative(('#eps',), 'a') == ('#empty',)
# assert derivative(('#union', ('#char', 'a'), ('#char', 'b')), 'a') == ('#union', ('#eps',), ('#empty',))
# assert derivative(('#star', ('#char', 'a')), 'a') == ('#concat', ('#eps',), ('#star', ('#char', 'a')))
# print('Exercice 2 : OK')

Exercice 3 — matches : reconnaître un mot par dérivées itérées

On reconnaît un mot \(s\) en dérivant successivement par chaque caractère puis en testant la nullabilité du résultat : \(s \in L(r) \iff \mathrm{nullable}(D_{s}(r))\). C’est exactement le mécanisme linéaire défendu en §1 (et l’analogue exécutable de l’Exercice Lean « construire la regex de “contient au moins un a” puis vérifier accepts »).

Objectif. Écrire matches(r, s) réutilisant derivative (Ex. 2) et nullable (Ex. 1).

Indice. Parcourir les caractères de s en remplaçant r par derivative(r, c) à chaque pas, puis retourner nullable(r).

Étapes. (1) Boucle for c in s: r = derivative(r, c) ; (2) retourner nullable(r).

def matches(r, s):
    # TODO etudiant : True ssi le mot s (iterable de caracteres) appartient a L(r).
    # Reutilise derivative (Exercice 2) et nullable (Exercice 1).
    # Indice : for c in s: r = derivative(r, c) ; puis return nullable(r).
    # Etape 1 : boucle de derivation. Etape 2 : return nullable(r).
    return None

# Tests (a decommenter) — le meme langage que l'Exercice Lean 'contient au moins un a' :
# assert matches(('#star', ('#char', 'a')), '') is True
# assert matches(('#star', ('#char', 'a')), 'aaa') is True
# assert matches(('#star', ('#char', 'a')), 'aab') is False
# assert matches(('#char', 'a'), 'a') is True
# assert matches(('#char', 'a'), 'b') is False
# print('Exercice 3 : OK')
Retour au sommet