369 lines
13 KiB
Python
369 lines
13 KiB
Python
#!/usr/bin/python3
|
|
# -*- coding: utf-8 -*-
|
|
|
|
__author__ = 'Éric W'
|
|
__date_creation__ = 'Fri Jan 22 17:18:09 2021'
|
|
__doc__ = """
|
|
:mod:`lambda_calcul` module
|
|
:author: {:s}
|
|
:creation date: {:s}
|
|
:last revision:
|
|
|
|
Module pour travailler avec le λ-calcul
|
|
|
|
|
|
""".format(__author__, __date_creation__)
|
|
|
|
from sly import Lexer, Parser
|
|
|
|
|
|
##################################################
|
|
# Partie Analyse Syntaxique
|
|
##################################################
|
|
|
|
class LambdaSyntaxError(Exception):
|
|
def __init__(self, msg):
|
|
self.message = msg
|
|
|
|
class Lambda_lexer(Lexer):
|
|
tokens = {VAR, LPAR, RPAR, LAMBDA, POINT}
|
|
VAR = r'[a-zA-Z][a-zA-Z0-9]*'
|
|
LPAR = r'\('
|
|
RPAR = r'\)'
|
|
LAMBDA = r'\!|λ'
|
|
POINT = r'\.'
|
|
ignore = ' \t'
|
|
|
|
@_(r'\n+')
|
|
def ignore_newline(self, t):
|
|
self.lineno += len(t.value)
|
|
|
|
def error(self, t):
|
|
raise LambdaSyntaxError('Caractère illégal : {:s} at position {:d}'.format(t.value[0],
|
|
t.index))
|
|
self.index += 1
|
|
|
|
lexer = Lambda_lexer()
|
|
|
|
class Lambda_parser(Parser):
|
|
''' Grammaire décrivant les λ-termes
|
|
term : VAR
|
|
| LAMBDA VAR POINT term
|
|
| LPAR term term RPAR
|
|
'''
|
|
tokens = Lambda_lexer.tokens
|
|
|
|
|
|
@_('VAR')
|
|
def term(self, p):
|
|
return (0, p[0])
|
|
|
|
@_('LAMBDA VAR POINT term')
|
|
def term(self, p):
|
|
return (1, p[1], p.term)
|
|
|
|
@_('LPAR term term RPAR')
|
|
def term(self, p):
|
|
return (2, p.term0, p.term1)
|
|
|
|
def error(self, p):
|
|
if p:
|
|
raise LambdaSyntaxError('{} inattendu en position {}'.format(p.type, p.index))
|
|
else:
|
|
raise LambdaSyntaxError('description inachevée')
|
|
|
|
parser = Lambda_parser()
|
|
|
|
##################################################
|
|
# Une classe pour représenter les λ-termes
|
|
##################################################
|
|
|
|
def _autre_variable(var, variables):
|
|
'''
|
|
renvoie var concaténé avec le premier numéro de sorte que le résultat ne soit pas dans variables
|
|
fonction utile pour les substitutions de termes
|
|
'''
|
|
n = 0
|
|
while var + '{:d}'.format(n) in variables:
|
|
n += 1
|
|
return var + '{:d}'.format(n)
|
|
|
|
class Lambda_termeError(Exception):
|
|
def __init__(self, msg):
|
|
self.message = msg
|
|
|
|
class Lambda_terme():
|
|
'''
|
|
Création de λ-terme
|
|
|
|
>>> T1 = Lambda_terme('z')
|
|
>>> print(T1)
|
|
z
|
|
>>> T2 = Lambda_terme('!x.(y x)')
|
|
>>> print(T2)
|
|
λx.(y x)
|
|
>>> T3 = Lambda_terme('(!x.(y x) z)')
|
|
>>> print(T3)
|
|
(λx.(y x) z)
|
|
|
|
Quelques prédicats
|
|
>>> [(t.est_variable(), t.est_abstraction(), t.est_application()) for t in (T1, T2, T3)]
|
|
[(True, False, False), (False, True, False), (False, False, True)]
|
|
|
|
Abstraction d'un terme
|
|
>>> T4 = T3.abstrait('z')
|
|
>>> print(T4)
|
|
λz.(λx.(y x) z)
|
|
|
|
Application d'un terme sur un autre
|
|
>>> T5 = T4.applique(Lambda_terme('t'))
|
|
>>> print(T5)
|
|
(λz.(λx.(y x) z) t)
|
|
|
|
Sous-termes d'un terme
|
|
>>> for t in T5.sous_termes():
|
|
... print(t)
|
|
(λz.(λx.(y x) z) t)
|
|
λz.(λx.(y x) z)
|
|
(λx.(y x) z)
|
|
λx.(y x)
|
|
(y x)
|
|
y
|
|
x
|
|
z
|
|
t
|
|
|
|
Autres prédicats
|
|
>>> [(t.est_redex(), t.est_forme_normale()) for t in (T1, T2, T3, T4, T5)]
|
|
[(False, True), (False, True), (True, False), (False, False), (True, False)]
|
|
|
|
Calcul de forme normale
|
|
|
|
>>> print(T5.forme_normale())
|
|
(y t)
|
|
>>> print(T5.forme_normale(verbose=True))
|
|
(λz.(λx.(y x) z) t)
|
|
1: ---> (λz.(λx.(y x) z) t)
|
|
2: ---> (λx.(y x) t)
|
|
3: ---> (y t)
|
|
Forme normale calculée : (y t)
|
|
(y t)
|
|
>>> OMEGA = Lambda_terme('(!x.(x x) !x.(x x))')
|
|
>>> print(OMEGA.forme_normale(verbose=True, nb_etapes_max=10))
|
|
(λx.(x x) λx.(x x))
|
|
1: ---> (λx.(x x) λx.(x x))
|
|
2: ---> (λx.(x x) λx.(x x))
|
|
3: ---> (λx.(x x) λx.(x x))
|
|
4: ---> (λx.(x x) λx.(x x))
|
|
5: ---> (λx.(x x) λx.(x x))
|
|
6: ---> (λx.(x x) λx.(x x))
|
|
7: ---> (λx.(x x) λx.(x x))
|
|
8: ---> (λx.(x x) λx.(x x))
|
|
9: ---> (λx.(x x) λx.(x x))
|
|
10: ---> (λx.(x x) λx.(x x))
|
|
Pas de forme normale atteinte après 10 étapes de réduction
|
|
None
|
|
'''
|
|
def __init__(self, *args):
|
|
nb_args = len(args)
|
|
if nb_args not in (1, 2, 3):
|
|
raise Lambda_termeError('Lambda_terme : Nbre arguments incorrect')
|
|
if nb_args == 1:
|
|
if not isinstance(args[0], str):
|
|
raise Lambda_termeError('Lambda_terme : type argument incorrect')
|
|
self._content = Lambda_terme._cree(parser.parse(lexer.tokenize(args[0])))
|
|
else:
|
|
categorie = args[0]
|
|
if categorie not in (0, 1, 2):
|
|
raise Lambda_termeError('categorie non valide')
|
|
if categorie == 0:
|
|
if nb_args != 2 or not isinstance(args[1], str):
|
|
raise Lambda_termeError('mauvaise construction pour une variable')
|
|
self._content = tuple(args)
|
|
elif categorie == 1:
|
|
if (nb_args != 3 or
|
|
not isinstance(args[1], str) or
|
|
not (isinstance(args[2], tuple) or isinstance(args[2], Lambda_terme))):
|
|
raise Lambda_termeError('mauvaise construction pour une abstraction')
|
|
self._content = (1, args[1],
|
|
Lambda_terme(*args[2]) if isinstance(args[2], tuple) else args[2])
|
|
else:
|
|
if (nb_args != 3 or
|
|
not (isinstance(args[1], tuple) or isinstance(args[1], Lambda_terme)) or
|
|
not (isinstance(args[2], tuple) or isinstance(args[2], Lambda_terme))):
|
|
raise Lambda_termeError('mauvaise construction pour une application')
|
|
self._content = (2,
|
|
Lambda_terme(*args[1]) if isinstance(args[1], tuple) else args[1],
|
|
Lambda_terme(*args[2]) if isinstance(args[2], tuple) else args[2])
|
|
|
|
@staticmethod
|
|
def _cree(descr):
|
|
if descr[0] == 0:
|
|
return descr
|
|
elif descr[0] == 1:
|
|
return (1, descr[1], Lambda_terme(*descr[2]))
|
|
else:
|
|
return (2, Lambda_terme(*descr[1]), Lambda_terme(*descr[2]))
|
|
|
|
def est_variable(self):
|
|
return self._content[0] == 0
|
|
|
|
def est_abstraction(self):
|
|
return self._content[0] == 1
|
|
|
|
def est_application(self):
|
|
return self._content[0] == 2
|
|
|
|
def __str__(self):
|
|
if self.est_variable():
|
|
return self._content[1]
|
|
elif self.est_abstraction():
|
|
return 'λ{:s}.{:s}'.format(self._content[1], str(self._content[2]))
|
|
else:
|
|
return '({:s} {:s})'.format(str(self._content[1]), str(self._content[2]))
|
|
|
|
def __eq__(self, terme):
|
|
if not isinstance(terme, Lambda_terme):
|
|
raise Lambda_termeError('Comparaison impossible')
|
|
if self.est_variable():
|
|
return terme.est_variable() and self._content[1] == terme._content[1]
|
|
elif self.est_application():
|
|
return (terme.est_application() and
|
|
self._content[1] == terme._content[1] and
|
|
self._content[2] == terme._content[2])
|
|
else:
|
|
return (terme.est_abstraction() and
|
|
self._content[2] == terme._content[2].subs(terme._content[1],
|
|
Lambda_terme(self._content[1])))
|
|
|
|
def applique(self, terme):
|
|
if not isinstance(terme, Lambda_terme):
|
|
raise Lambda_termeError('Application impossible')
|
|
return Lambda_terme(2, self, terme)
|
|
|
|
def abstrait(self, var):
|
|
if not isinstance(var, str):
|
|
raise Lambda_termeError("Variable d'Abstraction invalide")
|
|
return Lambda_terme(1, var, self)
|
|
|
|
def variables(self):
|
|
if self.est_variable():
|
|
return ({self._content[1]}, set())
|
|
elif self.est_application():
|
|
var_libres1, var_liees1 = self._content[1].variables()
|
|
var_libres2, var_liees2 = self._content[2].variables()
|
|
return (var_libres1.union(var_libres2),
|
|
var_liees1.union(var_liees2))
|
|
else:
|
|
var_libres, var_liees = self._content[2].variables()
|
|
if self._content[1] in var_libres:
|
|
var_libres.discard(self._content[1])
|
|
var_liees.add(self._content[1])
|
|
return (var_libres, var_liees)
|
|
|
|
def sous_termes(self):
|
|
if self.est_variable():
|
|
ss_termes = []
|
|
elif self.est_abstraction():
|
|
ss_termes = self._content[2].sous_termes()
|
|
else:
|
|
ss_termes = self._content[1].sous_termes()
|
|
ss_termes.extend(self._content[2].sous_termes())
|
|
return [self] + ss_termes
|
|
|
|
def est_redex(self):
|
|
return self.est_application() and self._content[1].est_abstraction()
|
|
|
|
def est_forme_normale(self):
|
|
if self.est_variable():
|
|
return True
|
|
elif self.est_abstraction():
|
|
return self._content[2].est_forme_normale()
|
|
else:
|
|
return (not self._content[1].est_abstraction() and
|
|
all(self._content[k].est_forme_normale() for k in (1, 2)))
|
|
|
|
def subs(self, var, terme):
|
|
if not isinstance(var, str):
|
|
raise Lambda_termeError('subst possible uniquement pour les variables')
|
|
if not isinstance(terme, Lambda_terme):
|
|
raise Lambda_termeError('subst possible uniquement sur un lambda-terme')
|
|
if self.est_variable():
|
|
if var == self._content[1]:
|
|
return terme
|
|
else:
|
|
return self
|
|
elif self.est_application():
|
|
return Lambda_terme(2,
|
|
self._content[1].subs(var, terme),
|
|
self._content[2].subs(var, terme))
|
|
else:
|
|
var_abstr = self._content[1]
|
|
corps_abstr = self._content[2]
|
|
var_libres_corps, _ = corps_abstr.variables()
|
|
if var == var_abstr or var not in var_libres_corps:
|
|
return self
|
|
elif var_abstr not in terme.variables()[0]:
|
|
return Lambda_terme(1, var_abstr, corps_abstr.subs(var, terme))
|
|
else:
|
|
nouvelle_var = _autre_variable(var_abstr, var_libres_corps)
|
|
return Lambda_terme(1,
|
|
nouvelle_var,
|
|
corps_abstr.subs(var_abstr,
|
|
Lambda_terme(0,nouvelle_var)).subs(var, terme))
|
|
|
|
def _reduit(self):
|
|
if self.est_variable():
|
|
return self, False
|
|
elif self.est_abstraction():
|
|
corps_reduit, est_reduit = self._content[2]._reduit()
|
|
return (Lambda_terme(1,
|
|
self._content[1],
|
|
corps_reduit) if est_reduit else self,
|
|
est_reduit)
|
|
else:
|
|
termegauche = self._content[1]
|
|
termedroit = self._content[2]
|
|
if termegauche.est_abstraction():
|
|
var_abstr = termegauche._content[1]
|
|
corps = termegauche._content[2]
|
|
return corps.subs(var_abstr, termedroit), True
|
|
else:
|
|
termegauche_reduit, est_reduit = termegauche._reduit()
|
|
if est_reduit:
|
|
return Lambda_terme(2, termegauche_reduit, termedroit), est_reduit
|
|
else:
|
|
termedroit_reduit, est_reduit = termedroit._reduit()
|
|
return (Lambda_terme(2,
|
|
termegauche,
|
|
termedroit_reduit) if est_reduit else self,
|
|
est_reduit)
|
|
|
|
def reduit(self):
|
|
return self._reduit()
|
|
|
|
def forme_normale(self, nb_etapes_max=100, verbose=False):
|
|
lambda_terme = self
|
|
etape = 0
|
|
forme_normale_atteinte = False
|
|
if verbose: print(lambda_terme)
|
|
while not forme_normale_atteinte and etape < nb_etapes_max:
|
|
etape += 1
|
|
terme_reduit, est_reduit = lambda_terme.reduit()
|
|
if verbose: print('{:3d}: ---> {:s}'.format(etape, str(terme_reduit)))
|
|
forme_normale_atteinte = terme_reduit.est_forme_normale()
|
|
lambda_terme = terme_reduit
|
|
if forme_normale_atteinte:
|
|
if verbose: print('Forme normale calculée : {:s}'.format(str(terme_reduit)))
|
|
return terme_reduit
|
|
else:
|
|
if verbose: print('Pas de forme normale atteinte après {:d} étapes de réduction'.format(etape))
|
|
return None
|
|
|
|
|
|
if __name__ == '__main__':
|
|
import doctest
|
|
doctest.testmod(optionflags=doctest.NORMALIZE_WHITESPACE | doctest.ELLIPSIS, verbose=True)
|
|
|
|
|