creation d'un module lambda_calcul indépendant du calepin
This commit is contained in:
Éric Wegrzynowski
parent
fa6b00e715
commit
83aa3a1406
2405
lambda_calcul.ipynb
2405
lambda_calcul.ipynb
File diff suppressed because it is too large
Load Diff
233
lambda_calcul.md
233
lambda_calcul.md
|
|
@ -16,250 +16,53 @@ jupyter:
|
|||
|
||||
# $\lambda$-calcul
|
||||
|
||||
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||||
## Analyseur lexical
|
||||
<!-- #endregion -->
|
||||
|
||||
```python
|
||||
from sly import Lexer
|
||||
from lambda_calcul import Lambda_terme
|
||||
```
|
||||
|
||||
```python
|
||||
class LambdaSyntaxError(Exception):
|
||||
def __init__(self, msg):
|
||||
self.message = msg
|
||||
```
|
||||
|
||||
```python
|
||||
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'
|
||||
|
||||
# Define a rule so we can track line numbers
|
||||
@_(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
|
||||
```
|
||||
|
||||
```python
|
||||
lexer = Lambda_lexer()
|
||||
```
|
||||
|
||||
```python
|
||||
l = list(lexer.tokenize('''((!x.(x x) y)
|
||||
λx.y)'''))
|
||||
l
|
||||
```
|
||||
|
||||
```python
|
||||
list(lexer.tokenize('!x.[y z]'))
|
||||
```
|
||||
|
||||
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||||
## Analyseur syntaxique
|
||||
<!-- #endregion -->
|
||||
|
||||
Voici la grammaire du langage décrivant les $\lambda$-termes
|
||||
|
||||
term ::= VAR | LAMBDA VAR POINT term | LPAR term term RPAR
|
||||
|
||||
```python
|
||||
from sly import Parser
|
||||
```
|
||||
|
||||
```python
|
||||
class Lambda_parser(Parser):
|
||||
tokens = Lambda_lexer.tokens
|
||||
|
||||
@_('VAR')
|
||||
def term(self, p):
|
||||
return Lambda_terme(0, p[0])
|
||||
|
||||
@_('LAMBDA VAR POINT term')
|
||||
def term(self, p):
|
||||
return Lambda_terme(1, p[1], p.term)
|
||||
|
||||
@_('LPAR term term RPAR')
|
||||
def term(self, p):
|
||||
return Lambda_terme(2, p.term0, p.term1)
|
||||
```
|
||||
|
||||
```python
|
||||
parser = Lambda_parser()
|
||||
```
|
||||
|
||||
## La classe `Lambda_terme`
|
||||
|
||||
```python
|
||||
def autre_variable(var, variables):
|
||||
n = 0
|
||||
while var + '{:d}'.format(n) in variables:
|
||||
n += 1
|
||||
return var + '{:d}'.format(n)
|
||||
|
||||
class Lambda_terme():
|
||||
def __init__(self, categorie, *args):
|
||||
if categorie not in (0, 1, 2):
|
||||
raise Exception('categorie non valide')
|
||||
if categorie == 0:
|
||||
if len(args) != 1 or not isinstance(args[0], str):
|
||||
raise Exception('mauvaise construction pour une variable')
|
||||
elif categorie == 1:
|
||||
if len(args) != 2 or not isinstance(args[0], str) or not isinstance(args[1], Lambda_terme):
|
||||
raise Exception('mauvaise construction pour une abstraction')
|
||||
else:
|
||||
if len(args) != 2 or not isinstance(args[0], Lambda_terme) or not isinstance(args[1], Lambda_terme):
|
||||
raise Exception('mauvaise construction pour une application')
|
||||
self._content = (categorie,) + tuple(args)
|
||||
|
||||
@staticmethod
|
||||
def cree(descr):
|
||||
return parser.parse(lexer.tokenize(descr))
|
||||
|
||||
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 applique(self, terme):
|
||||
if not isinstance(terme, Lambda_terme):
|
||||
raise Exception('Application impossible')
|
||||
return Lambda_terme(2, self, terme)
|
||||
|
||||
def abstrait(self, var):
|
||||
if not isinstance(var, str):
|
||||
raise Exception("Variable d'Abstraction invalide")
|
||||
return Lambda_terme(1, var, self)
|
||||
|
||||
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 variables_libres(self):
|
||||
if self.est_variable():
|
||||
return {self._content[1]}
|
||||
elif self.est_application():
|
||||
var_libres = self._content[2].variables_libres()
|
||||
return var_libres.union(self._content[1].variables_libres())
|
||||
else:
|
||||
var_libres = self._content[2].variables_libres()
|
||||
var_libres.discard(self._content[1])
|
||||
return var_libres
|
||||
|
||||
def subs(self, var, terme):
|
||||
if not isinstance(var, str):
|
||||
raise Exception('subst possible uniquement pour les variables')
|
||||
if not isinstance(terme, Lambda_terme):
|
||||
raise Exception('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_libres()
|
||||
if var == var_abstr or var not in var_libres_corps:
|
||||
return self
|
||||
elif var_abstr not in terme.variables_libres():
|
||||
return Lambda_terme(1, var_abstr, corps_abstr.subs(var, terme))
|
||||
else:
|
||||
nouvelle_var = autre_variable(var_abstr, corps_abstr.variables_libres())
|
||||
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 __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]))
|
||||
```
|
||||
|
||||
```python
|
||||
T1 = Lambda_terme(0, "x")
|
||||
T2 = Lambda_terme(1, "x", T1)
|
||||
T3 = Lambda_terme.cree('(!x.x x)')
|
||||
T3 = Lambda_terme(2, T2, T1)
|
||||
T4 = Lambda_terme.cree('!x.(x x)')
|
||||
```
|
||||
|
||||
```python
|
||||
print(T1)
|
||||
print(T2)
|
||||
print(T3)
|
||||
print(T4)
|
||||
```
|
||||
|
||||
```python
|
||||
tuple(t.est_variable() for t in (T1, T2, T3))
|
||||
tuple(t.est_variable() for t in (T1, T2, T3, T4))
|
||||
```
|
||||
|
||||
```python
|
||||
tuple(t.est_abstraction() for t in (T1, T2, T3))
|
||||
tuple(t.est_abstraction() for t in (T1, T2, T3, T4))
|
||||
```
|
||||
|
||||
```python
|
||||
tuple(t.est_application() for t in (T1, T2, T3))
|
||||
tuple(t.est_application() for t in (T1, T2, T3, T4))
|
||||
```
|
||||
|
||||
```python
|
||||
tuple(t.est_redex() for t in (T1, T2, T3))
|
||||
tuple(t.est_redex() for t in (T1, T2, T3, T4))
|
||||
```
|
||||
|
||||
```python
|
||||
tuple(t.est_forme_normale() for t in (T1, T2, T3))
|
||||
tuple(t.est_forme_normale() for t in (T1, T2, T3, T4))
|
||||
```
|
||||
|
||||
```python
|
||||
tuple(t.variables_libres() for t in (T1, T2, T3))
|
||||
tuple(t.variables_libres() for t in (T1, T2, T3, T4))
|
||||
```
|
||||
|
||||
```python
|
||||
|
|
@ -268,10 +71,10 @@ print(T1, '-->', T1.subs('x', Lambda_terme.cree('(y x)')))
|
|||
```
|
||||
|
||||
```python
|
||||
T4 = Lambda_terme.cree('!x.y')
|
||||
print(T4, '-->', T4.subs('x', Lambda_terme.cree('(y z)')))
|
||||
print(T4, '-->', T4.subs('y', Lambda_terme.cree('(t z)')))
|
||||
print(T4, '-->', T4.subs('y', Lambda_terme.cree('(x z)')))
|
||||
T5 = Lambda_terme.cree('!x.y')
|
||||
print(T5, '-->', T5.subs('x', Lambda_terme.cree('(y z)')))
|
||||
print(T5, '-->', T5.subs('y', Lambda_terme.cree('(t z)')))
|
||||
print(T5, '-->', T5.subs('y', Lambda_terme.cree('(x z)')))
|
||||
```
|
||||
|
||||
```python
|
||||
|
|
@ -999,3 +802,11 @@ phiExpoMod = lambda x: lambda y: lambda z: lambda t: 1 if z == 0 else (lambda u:
|
|||
```python
|
||||
fix_curry(phiExpoMod)(2)(10)(1000)
|
||||
```
|
||||
|
||||
```python
|
||||
|
||||
```
|
||||
|
||||
```python
|
||||
|
||||
```
|
||||
|
|
|
|||
|
|
@ -0,0 +1,214 @@
|
|||
#!/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):
|
||||
tokens = Lambda_lexer.tokens
|
||||
|
||||
@_('VAR')
|
||||
def term(self, p):
|
||||
return Lambda_terme(0, p[0])
|
||||
|
||||
@_('LAMBDA VAR POINT term')
|
||||
def term(self, p):
|
||||
return Lambda_terme(1, p[1], p.term)
|
||||
|
||||
@_('LPAR term term RPAR')
|
||||
def term(self, p):
|
||||
return Lambda_terme(2, p.term0, p.term1)
|
||||
|
||||
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
|
||||
'''
|
||||
n = 0
|
||||
while var + '{:d}'.format(n) in variables:
|
||||
n += 1
|
||||
return var + '{:d}'.format(n)
|
||||
|
||||
class Lambda_terme():
|
||||
def __init__(self, categorie, *args):
|
||||
if categorie not in (0, 1, 2):
|
||||
raise Exception('categorie non valide')
|
||||
if categorie == 0:
|
||||
if len(args) != 1 or not isinstance(args[0], str):
|
||||
raise Exception('mauvaise construction pour une variable')
|
||||
elif categorie == 1:
|
||||
if (len(args) != 2 or
|
||||
not isinstance(args[0], str) or
|
||||
not isinstance(args[1], Lambda_terme)):
|
||||
raise Exception('mauvaise construction pour une abstraction')
|
||||
else:
|
||||
if (len(args) != 2 or
|
||||
not isinstance(args[0], Lambda_terme) or
|
||||
not isinstance(args[1], Lambda_terme)):
|
||||
raise Exception('mauvaise construction pour une application')
|
||||
self._content = (categorie,) + tuple(args)
|
||||
|
||||
@staticmethod
|
||||
def cree(descr):
|
||||
return parser.parse(lexer.tokenize(descr))
|
||||
|
||||
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 applique(self, terme):
|
||||
if not isinstance(terme, Lambda_terme):
|
||||
raise Exception('Application impossible')
|
||||
return Lambda_terme(2, self, terme)
|
||||
|
||||
def abstrait(self, var):
|
||||
if not isinstance(var, str):
|
||||
raise Exception("Variable d'Abstraction invalide")
|
||||
return Lambda_terme(1, var, self)
|
||||
|
||||
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 variables_libres(self):
|
||||
if self.est_variable():
|
||||
return {self._content[1]}
|
||||
elif self.est_application():
|
||||
var_libres = self._content[2].variables_libres()
|
||||
return var_libres.union(self._content[1].variables_libres())
|
||||
else:
|
||||
var_libres = self._content[2].variables_libres()
|
||||
var_libres.discard(self._content[1])
|
||||
return var_libres
|
||||
|
||||
def subs(self, var, terme):
|
||||
if not isinstance(var, str):
|
||||
raise Exception('subst possible uniquement pour les variables')
|
||||
if not isinstance(terme, Lambda_terme):
|
||||
raise Exception('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_libres()
|
||||
if var == var_abstr or var not in var_libres_corps:
|
||||
return self
|
||||
elif var_abstr not in terme.variables_libres():
|
||||
return Lambda_terme(1, var_abstr, corps_abstr.subs(var, terme))
|
||||
else:
|
||||
nouvelle_var = _autre_variable(var_abstr, corps_abstr.variables_libres())
|
||||
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 __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]))
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
import doctest
|
||||
doctest.testmod(optionflags=doctest.NORMALIZE_WHITESPACE | doctest.ELLIPSIS, verbose=False)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue