1002 lines
21 KiB
Markdown
1002 lines
21 KiB
Markdown
|
---
|
||
|
jupyter:
|
||
|
jupytext:
|
||
|
formats: ipynb,md
|
||
|
text_representation:
|
||
|
extension: .md
|
||
|
format_name: markdown
|
||
|
format_version: '1.2'
|
||
|
jupytext_version: 1.6.0
|
||
|
kernelspec:
|
||
|
display_name: Python 3
|
||
|
language: python
|
||
|
name: python3
|
||
|
---
|
||
|
|
||
|
|
||
|
# $\lambda$-calcul
|
||
|
|
||
|
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||
|
## Analyseur lexical
|
||
|
<!-- #endregion -->
|
||
|
|
||
|
```python
|
||
|
from sly import Lexer
|
||
|
```
|
||
|
|
||
|
```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)')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(T1)
|
||
|
print(T2)
|
||
|
print(T3)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(t.est_variable() for t in (T1, T2, T3))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(t.est_abstraction() for t in (T1, T2, T3))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(t.est_application() for t in (T1, T2, T3))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(t.est_redex() for t in (T1, T2, T3))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(t.est_forme_normale() for t in (T1, T2, T3))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(t.variables_libres() for t in (T1, T2, T3))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(T1, '-->', T1.subs('y', Lambda_terme.cree('(y x)')))
|
||
|
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)')))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(T3, '-->', T3.subs('y', Lambda_terme.cree('(y x)')))
|
||
|
print(T3, '-->', T3.subs('x', Lambda_terme.cree('(y x)')))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
OMEGA = Lambda_terme.cree('(!x.(x x) !x.(x x))')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(OMEGA)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
OMEGA.est_redex()
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
OMEGA.est_forme_normale()
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
OMEGA.variables_libres()
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
res, est_red = OMEGA.reduit()
|
||
|
print(res)
|
||
|
print(est_red)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
res, est_red = Lambda_terme.cree('(!x.(eric x) vero)').reduit()
|
||
|
print(res, est_red)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
def calcul(lambda_terme, nb_etapes_max=100, verbose=False):
|
||
|
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(lambda_terme), str(terme_reduit)))
|
||
|
forme_normale_atteinte = not est_reduit
|
||
|
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
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(OMEGA, nb_etapes_max=10, verbose=True)
|
||
|
```
|
||
|
|
||
|
## Entiers, successeurs, addition, multiplication et exponentiation
|
||
|
|
||
|
```python
|
||
|
ZERO = Lambda_terme.cree('!f.!x.x')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
UN = Lambda_terme.cree('!f.!x.(f x)')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
DEUX = Lambda_terme.cree('!f.!x.(f (f x))')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
SUC = Lambda_terme.cree('!n.!f.!x.(f ((n f) x))')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
TROIS = calcul(SUC.applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(TROIS.applique(SUC).applique(ZERO), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
ADD = Lambda_terme.cree('!n.!m.!f.!x.((n f) ((m f) x))')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
QUATRE = calcul(ADD.applique(UN).applique(TROIS), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
CINQ = calcul(ADD.applique(TROIS).applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
SEPT = calcul(ADD.applique(QUATRE).applique(TROIS), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
MUL = Lambda_terme.cree('!n.!m.!f.(n (m f))')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
SIX = calcul(MUL.applique(DEUX).applique(TROIS), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
EXP = Lambda_terme.cree('!n.!m.(m n)')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
HUIT = calcul(EXP.applique(DEUX).applique(TROIS), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
NEUF = calcul(EXP.applique(TROIS).applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
## Booléens, opérateurs logiques et conditionnelles
|
||
|
|
||
|
```python
|
||
|
VRAI = Lambda_terme.cree('!x.!y.x')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
FAUX = Lambda_terme.cree('!x.!y.y')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
COND = Lambda_terme.cree('!c.!a.!s.((c a) s)')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(COND.applique(VRAI).applique(UN).applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(COND.applique(FAUX).applique(UN).applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
ET = COND.applique(Lambda_terme.cree('a')).applique(Lambda_terme.cree('b')).applique(FAUX).abstrait('b').abstrait('a')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(ET)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(ET.applique(VRAI).applique(VRAI), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(ET.applique(VRAI).applique(FAUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(ET.applique(FAUX).applique(VRAI), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(ET.applique(FAUX).applique(FAUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
OU = COND.applique(Lambda_terme.cree('a')).applique(VRAI).applique(Lambda_terme.cree('b')).abstrait('b').abstrait('a')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(OU.applique(VRAI).applique(VRAI), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(OU.applique(VRAI).applique(FAUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(OU.applique(FAUX).applique(VRAI), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(OU.applique(FAUX).applique(FAUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
NON = COND.applique(Lambda_terme.cree('a')).applique(FAUX).applique(VRAI).abstrait('a')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(NON.applique(VRAI), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(NON.applique(FAUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
NUL = Lambda_terme.cree('!n.((n !x.{:s}) {:s})'.format(str(FAUX), str(VRAI)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(NUL)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(NUL.applique(ZERO), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(NUL.applique(TROIS), verbose=True)
|
||
|
```
|
||
|
|
||
|
## Couples
|
||
|
|
||
|
```python
|
||
|
CONS = COND.applique(Lambda_terme.cree('s')).applique(Lambda_terme.cree('x')).applique(Lambda_terme.cree('y')).abstrait('s').abstrait('y').abstrait('x')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(CONS)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
UN_DEUX = calcul(CONS.applique(UN).applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
CAR = Lambda_terme.cree('c').applique(VRAI).abstrait('c')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(CAR)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(CAR.applique(UN_DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
CDR = Lambda_terme.cree('c').applique(FAUX).abstrait('c')
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(CDR.applique(UN_DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
M_PRED = Lambda_terme.cree('!n.(CAR ((n !c.((CONS (CDR c)) (SUC (CDR c)))) ((CONS ZERO) ZERO)))')
|
||
|
print(M_PRED)
|
||
|
PRED = M_PRED.subs('CAR', CAR).subs('CONS', CONS).subs('CDR', CDR).subs('SUC', SUC).subs('ZERO', ZERO)
|
||
|
print(PRED)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(PRED.applique(DEUX), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(PRED.applique(ZERO), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
M_SUB = Lambda_terme.cree('!n.!m.((m PRED) n)')
|
||
|
print(M_SUB)
|
||
|
SUB = M_SUB.subs('PRED', PRED)
|
||
|
print(SUB)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(SUB.applique(TROIS).applique(UN), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
M_INF = Lambda_terme.cree('!n.!m.(NUL ((SUB m) n))')
|
||
|
print(M_INF)
|
||
|
INF = M_INF.subs('NUL', NUL).subs('SUB', SUB)
|
||
|
#lambda n: lambda m: est_nul(sub(m)(n))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(INF.applique(TROIS).applique(UN), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(INF.applique(UN).applique(TROIS), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(INF.applique(UN).applique(UN), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
M_EGAL = Lambda_terme.cree('!n.!m.((ET ((INF n) m)) ((INF m) n))')
|
||
|
print(M_EGAL)
|
||
|
EGAL = M_EGAL.subs('ET', ET).subs('INF', INF)
|
||
|
print(EGAL)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(EGAL.applique(UN).applique(UN)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(EGAL.applique(UN).applique(DEUX)))
|
||
|
```
|
||
|
|
||
|
## Itération
|
||
|
|
||
|
```python
|
||
|
M_FACTv1 = Lambda_terme.cree('!n.(CDR ((n !c.((CONS (SUC (CAR c))) ((MUL (SUC (CAR c))) (CDR c)))) ((CONS ZERO) UN)))')
|
||
|
print(M_FACTv1)
|
||
|
FACTv1 = M_FACTv1.subs('CONS', CONS).subs('CAR', CAR).subs('CDR', CDR).subs('SUC', SUC).subs('MUL', MUL).subs('UN', UN).subs('ZERO', ZERO)
|
||
|
print(FACTv1)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv1.applique(ZERO)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv1.applique(UN)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv1.applique(DEUX)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv1.applique(DEUX), nb_etapes_max=200))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv1.applique(TROIS), nb_etapes_max=500))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv1.applique(QUATRE), nb_etapes_max=1700))
|
||
|
```
|
||
|
|
||
|
## Et la récursivité ?
|
||
|
|
||
|
```python
|
||
|
M_PHI_FACT = Lambda_terme.cree('!f.!n.(((COND ((EGAL n) ZERO)) UN) ((MUL n) (f (PRED n))))')
|
||
|
print(M_PHI_FACT)
|
||
|
PHI_FACT = M_PHI_FACT.subs('COND', COND).subs('EGAL', EGAL).subs('ZERO', ZERO).subs('UN', UN).subs('MUL', MUL).subs('PRED', PRED)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
BOTTOM = Lambda_terme.cree('!y.OMEGA').subs('OMEGA', OMEGA)
|
||
|
print(BOTTOM)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
FACT0 = PHI_FACT.applique(BOTTOM)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACT0.applique(ZERO)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(FACT0.applique(UN), verbose=True)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
FACT1 = PHI_FACT.applique(FACT0)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACT1.applique(ZERO)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACT1.applique(UN), nb_etapes_max=200))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
FIX_CURRY = Lambda_terme.cree('!f.(!x.(f (x x)) !x.(f (x x)))')
|
||
|
print(FIX_CURRY)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
FACTv2 = FIX_CURRY.applique(PHI_FACT)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv2.applique(ZERO)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv2.applique(UN), nb_etapes_max=200))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv2.applique(DEUX), nb_etapes_max=700))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv2.applique(TROIS), nb_etapes_max=4000))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
print(calcul(FACTv2.applique(QUATRE), nb_etapes_max=25000))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
PF = FIX_CURRY.applique(Lambda_terme.cree('M'))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
calcul(PF, verbose=True, nb_etapes_max=10)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
|
||
|
```
|
||
|
|
||
|
|
||
|
# $\lambda$-calcul avec les lambda-expressions de Python
|
||
|
|
||
|
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||
|
## Les entiers de Church
|
||
|
<!-- #endregion -->
|
||
|
|
||
|
```python
|
||
|
zero = lambda f: lambda x: x
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
un = lambda f: lambda x: f(x)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
deux = lambda f: lambda x: f(f(x))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
trois = lambda f: lambda x: f(f(f(x)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
def entier_church_en_int(ec):
|
||
|
return ec(lambda n: n+1)(0)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(entier_church_en_int(n) for n in (zero, un, deux, trois))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
suc = lambda n: lambda f: lambda x: f(n(f)(x))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(entier_church_en_int(suc(n)) for n in (zero, un, deux, trois))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
def int_en_entier_church(n):
|
||
|
if n == 0:
|
||
|
return zero
|
||
|
else:
|
||
|
return suc(int_en_entier_church(n - 1))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(entier_church_en_int(int_en_entier_church(n)) for n in range(10))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
add = lambda n: lambda m: lambda f: lambda x: n(f)(m(f)(x))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
cinq = add(deux)(trois)
|
||
|
entier_church_en_int(cinq)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
mul = lambda n: lambda m: lambda f: n(m(f))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
six = mul(deux)(trois)
|
||
|
entier_church_en_int(six)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
exp = lambda n: lambda m: m(n)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
huit = exp(deux)(trois)
|
||
|
entier_church_en_int(huit)
|
||
|
```
|
||
|
|
||
|
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||
|
## Les booléens
|
||
|
<!-- #endregion -->
|
||
|
|
||
|
```python
|
||
|
vrai = lambda x: lambda y: x
|
||
|
faux = lambda x: lambda y: y
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
def booleen_en_bool(b):
|
||
|
return b(True)(False)
|
||
|
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(b) for b in (vrai, faux))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
cond = lambda c: lambda a: lambda s: c(a)(s)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
cond(vrai)(1)(2)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
cond(faux)(1)(2)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
cond(vrai)(1)(1/0)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
non = lambda b: cond(b)(faux)(vrai)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(non(b)) for b in (vrai, faux))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
et = lambda b1: lambda b2: cond(b1)(b2)(faux)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(et(b1)(b2)) for b1 in (vrai, faux) for b2 in (vrai, faux))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
ou = lambda b1: lambda b2: cond(b1)(vrai)(b2)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(ou(b1)(b2)) for b1 in (vrai, faux) for b2 in (vrai, faux))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
est_nul = lambda n : n(lambda x: faux)(vrai)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(est_nul(n)) for n in (zero, un, deux, trois, cinq, six, huit))
|
||
|
```
|
||
|
|
||
|
## Les couples
|
||
|
|
||
|
```python
|
||
|
cons = lambda x: lambda y: lambda z: z(x)(y)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
un_deux = cons(un)(deux)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
car = lambda c: c(vrai)
|
||
|
cdr = lambda c: c(faux)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
entier_church_en_int(car(un_deux)), entier_church_en_int(cdr(un_deux))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
pred = lambda n: car(n(lambda c: cons(cdr(c))(suc(cdr(c))))(cons(zero)(zero)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(entier_church_en_int(pred(int_en_entier_church(n))) for n in range(10))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
sub = lambda n: lambda m: m(pred)(n)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
entier_church_en_int(sub(huit)(trois))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
est_inf_ou_egal = lambda n: lambda m: est_nul(sub(m)(n))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(est_inf_ou_egal(cinq)(int_en_entier_church(n))) for n in range(10))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
est_egal = lambda n: lambda m: et(est_inf_ou_egal(n)(m))(est_inf_ou_egal(m)(n))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(booleen_en_bool(est_egal(cinq)(int_en_entier_church(n))) for n in range(10))
|
||
|
```
|
||
|
|
||
|
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||
|
## Itération
|
||
|
<!-- #endregion -->
|
||
|
|
||
|
```python
|
||
|
fact = lambda n: cdr(n(lambda c: (cons(suc(car(c)))(mul(suc(car(c)))(cdr(c)))))(cons(zero)(un)))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(entier_church_en_int(fact(int_en_entier_church(n))) for n in range(7))
|
||
|
```
|
||
|
|
||
|
## Combinateur de point fixe
|
||
|
|
||
|
```python
|
||
|
phi_fact = lambda f: lambda n: 1 if n == 0 else n*f(n-1)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
bottom = lambda x: (lambda y: y(y))(lambda y:y(y))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
f0 = phi_fact(bottom)
|
||
|
f1 = phi_fact(f0)
|
||
|
f2 = phi_fact(f1)
|
||
|
f3 = phi_fact(f2)
|
||
|
f4 = phi_fact(f3)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(f4(n) for n in range(4))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
def fact_rec(n):
|
||
|
if n == 0:
|
||
|
return 1
|
||
|
else:
|
||
|
return n * fact_rec(n - 1)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
fact2 = phi_fact(fact_rec)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(fact2(n) for n in range(7))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
fix_curry = lambda f: (lambda x: lambda y: f(x(x))(y))(lambda x: lambda y: f(x(x))(y))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
fact3 = fix_curry(phi_fact)
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
tuple(fact3(n) for n in range(7))
|
||
|
```
|
||
|
|
||
|
<!-- #region toc-hr-collapsed=true toc-nb-collapsed=true -->
|
||
|
## Un programme obscur
|
||
|
<!-- #endregion -->
|
||
|
|
||
|
```python
|
||
|
print((lambda x: (lambda y: lambda z: x(y(y))(z))(lambda y: lambda z: x(y(y))(z)))
|
||
|
(lambda x: lambda y: '' if y == [] else chr(y[0])+x(y[1:]))
|
||
|
(((lambda x: (lambda y: lambda z: x(y(y))(z)) (lambda y: lambda z: x(y(y))(z)))
|
||
|
(lambda x: lambda y: lambda z: [] if z == [] else [y(z[0])]+x(y)(z[1:])))
|
||
|
(lambda x: (lambda x: (lambda y: lambda z: x(y(y))(z))(lambda y: lambda z: x(y(y))(z)))
|
||
|
(lambda x: lambda y: lambda z: lambda t: 1 if t == 0 else (lambda x: ((lambda u: 1 if u == 0 else z)(t % 2)) * x * x % y)
|
||
|
(x(y)(z)(t // 2)))(989)(x)(761))
|
||
|
([377, 900, 27, 27, 182, 647, 163, 182, 390, 27, 726, 937])))
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
phiListEnChaine = lambda x: lambda y: '' if y == [] else chr(y[0]) + x(y[1:])
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
fix_curry(phiListEnChaine)([65+k for k in range(26)])
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
phiMap = lambda x: lambda y: lambda z: [] if z == [] else [y(z[0])] + x(y)(z[1:])
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
fix_curry(phiMap)(lambda x: x*x)([1, 2, 3, 4])
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
phiExpoMod = lambda x: lambda y: lambda z: lambda t: 1 if z == 0 else (lambda u: 1 if u == 0 else y)(z % 2) * x(y)(z//2)(t) ** 2 % t
|
||
|
```
|
||
|
|
||
|
```python
|
||
|
fix_curry(phiExpoMod)(2)(10)(1000)
|
||
|
```
|