Select Git revision
SplitTransModule.cpp
logic.py 17.14 KiB
#les lambda termes et les variables sont représentés par des listes dont le premier element indique le type du lambda terme et le deuxieme ses composants
# Constantes
VAR = 'variable'
ABS = "abstraction"
APP = "application"
var_counter = 0
#prend en argument une chaine de caractère et renvoie une variable
def new_var(x):
return [VAR, x]
# prend en argument deux lamba termes/ variables et renvoie le lambda terme AB
def new_app(A, B): return [APP, A , B]
#prend en argument une variable x et un lambda terme/variable A et retourne le lambda terme (lambda x. A)
def new_abs(x,A):
assert isVariable(x), "argument is not a variable!"
return [ABS, x, A]
# retourne le type du lambda terme mis en parametre
def getType(P): return P[0]
# verifie si terme est de type variable
def isVariable(terme): return getType(terme) == VAR
# True si terme est une application, False sinon
def isApplication(terme): return getType(terme) == APP
#True si terme est un lambda terme de la forme (lambda x . A)
def isAbstraction(terme): return getType(terme) == ABS
# True si terme est un lambda terme de n'importe quelle forme
def isLambdaTerm(terme): return isVariable(terme) or isAbstraction(terme) or isApplication(terme)
# Prends en parametre une variable P et retourne une liste contenant le nom de la variable
def getVariablesFromVar(terme):
assert isVariable(terme), "argument is not a variable!"
return [terme]
# Prends en parametre une abstraction 'P' et renvoie une liste des nom des variables que cette abstraction contient
def getVariablesFromAbs(terme):
assert isAbstraction(terme), "argument is not an abstraction!"
return getVariables(terme[1]) + getVariables(terme[2])
# Prends en parametre une application P (A B) et nous rend le premier terme A de cette application
def getFirstTerm(app):
assert isApplication(app), "argument is not an application!"
return app[1]
# Prends en parametre une application P (A B) et nous rend le deuxieme terme B de cette application
def getSecondTerm(app):
assert isApplication(app), "argument is not an application!"
return app[2]
# Prends en parametre une application (A B) et nous rend une liste des variables que contient P(cad les variables de A et de B)
def getVariablesFromApp(terme):
assert isApplication(terme), "argument is not an application!"
variables = []
first = getFirstTerm(terme)
second = getSecondTerm(terme)
variables += getVariables(first) + getVariables(second)
return variables
# Prends en parametre n'importe qu'elle expression 'P' (Lambda-Term) et nous rend les variables de cette expression
def getVariables(terme):
assert isLambdaTerm(terme), "argument is not a lambda term!"
if isVariable(terme):
return getVariablesFromVar(terme)
elif isAbstraction(terme):
return getVariablesFromAbs(terme)
elif isApplication(terme):
return getVariablesFromApp(terme)
# Prends en parametre une abstraction 'terme1' et n'importe quel lambda-term 'terme2' et nous rend une liste des variables communes entre terme1 et terme2, sinon elle retourne une liste vide
def getCommonVariables(terme1,terme2):
assert isAbstraction(terme1), "argument is not an abstraction!"
return [i for i in getVariables(terme1) if i in getVariables(terme2)]
return set(getVariables(terme1)).intersection(getVariables(terme2))
# Prends en parametre une abstraction 'terme1' et un lambda-term 'terme2' et nous rend True si terme2 contient des variables de terme1
def isCommonVariables(terme1,terme2):
return not(len(getCommonVariables(terme1,terme2)) == 0)
# Prends en parametre une abstraction 'A' et nous rend la liste des variables de l'entree de l'abstraction
def getInputVariablesFromAbs(A):
assert isAbstraction(A), "argument is not an abstraction!"
return getVariables(A[1])
# Prends en parametre une abstraction 'A' et nous rend la liste des variables de la sortie de l'abstraction
def getOutputVariablesFromAbs(A):
assert isAbstraction(A), "argument is not an abstraction!"
return getVariables(A[2])
# retourne la variable en entree de l'abstraction 'A'
def getInputFromAbs(A):
assert isAbstraction(A), "argument is not an abstraction!"
return A[1]
# retourne les sorties de l'abstraction 'A'
def getOutputFromAbs(A):
assert isAbstraction(A), "argument is not an abstraction!"
return A[2]
# Prends en parametre une une variable a changer, une nouvelle variable et un lambda terme et remplace la variable a changer par la nouvelle variable dans le lambda term.
def substitute(var_a_changer,subs_terme, terme):
if terme == var_a_changer:
return subs_terme.copy()
elif isVariable(terme):
return terme.copy()
elif isApplication(terme):
return new_app(substitute(var_a_changer,subs_terme,getFirstTerm(terme)),substitute(var_a_changer,subs_terme,getSecondTerm(terme)))
if getInputFromAbs(terme) == var_a_changer:
return terme.copy()
return new_abs(getInputFromAbs(terme).copy(),substitute(var_a_changer,subs_terme,getOutputFromAbs(terme).copy()))
#Prends en parametre un lambda terme "grandTerme" et nous retourne lee variables liees de ce terme.
def getBoundVariables(grandTerme):
vars = []
if isAbstraction(grandTerme):
vars += getInputVariablesFromAbs(grandTerme)
A = getOutputFromAbs(grandTerme)
if isAbstraction(A) or isApplication(A):
vars += getBoundVariables(A)
if isApplication(grandTerme):
vars += getBoundVariables(getFirstTerm(grandTerme))
vars += getBoundVariables(getSecondTerm(grandTerme))
return (vars)
#prend en parametre une variable et retourne une variable fraiche a partir du dictionnaire counters
def freshVar():
global var_counter
var_counter += 1
return (var_counter -1)
# Prends en parametre un lambda term 't' et nous retourne une expression equivalente a 't' mais avec une variable fraiche au lieu de la variable 'var'
def alpha_rename(t,var):
if isVariable(t):
return t.copy()
elif isAbstraction(t):
x = getInputFromAbs(t)
A = getOutputFromAbs(t)
if x == var:
x1 = new_var(freshVar())
return new_abs(x1,substitute(var,x1,getOutputFromAbs(t)))
else:
return new_abs(x.copy(),alpha_rename(A,var))
A = getFirstTerm(t)
B = getSecondTerm(t)
return new_app(alpha_rename(A,var),alpha_rename(B,var))
#Renvoie un lambda terme qui represente le terme t une fois réduit
def beta_reduction(t):
if isVariable(t):
return None
elif isAbstraction(t):
x = getInputFromAbs(t)
A = getOutputFromAbs(t)
B = beta_reduction(A)
if B != None:
return new_abs(x.copy(),B) ### x.copy() sont inutiles car on ne change jamais le tableau de variables
else:
return None
elif isApplication(t):
A1 = getFirstTerm(t)
B1 = getSecondTerm(t)
A2 = beta_reduction(A1)
if A2 != None:
return (new_app(A2,B1))
elif A2 == None:
B2 = beta_reduction(B1)
if B2 != None:
return (new_app(A1,B2))
elif isAbstraction(A1):
x1 = getInputFromAbs(A1)
C = getOutputFromAbs(A1)
communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
if communBoundVars == []:
return substitute(x1,B1,C)
else:
terme=A1
for var in communBoundVars:
terme=alpha_rename(terme,(var))
return substitute(getInputFromAbs(terme),B1,getOutputFromAbs(terme))
else:
return None
import image_maker
image_counter = 0
def captureImage(terme):
global image_counter
image_maker.saveImage(image_maker.createImage(terme),str(image_counter))
image_counter += 1
def beta_reduction_totale(terme):
captureImage(terme)
if beta_reduction(terme) != None:
return beta_reduction_totale(beta_reduction(terme))
return (terme)
numbers_to_letters = {
0:'x',
1:'y',
2:'z',
3:'q',
4:'w',
5:'e',
6:'r',
7:'t',
8:'u',
9:'p',
10:'d',
11:'a',
12:'k',
13:'m',
14:'n',
15:'v',
16:'f',
17:'ç'
}
def to_string_var(terme):
assert (isVariable(terme)), 'The argument is not a variable'
return (numbers_to_letters[terme[1]])
def to_string_abs(terme):
assert (isAbstraction(terme)), 'The argument is not an Abstraction'
return "\u03BB"+to_string(getInputFromAbs(terme))+"."+to_string(getOutputFromAbs(terme))
def to_string_app(terme):
assert (isApplication(terme)), 'The argument is not an application' #ons econd term if application / no () over variable/ if ABS inside APP ()
premier_terme = ''
deuxieme_terme = ''
if isVariable(getFirstTerm(terme)):
premier_terme += to_string(getFirstTerm(terme))
elif isAbstraction(getFirstTerm(terme)):
premier_terme += "("+to_string(getFirstTerm(terme))+")"
elif isApplication(getFirstTerm(terme)):
premier_terme += to_string(getFirstTerm(terme))
if isVariable(getSecondTerm(terme)):
deuxieme_terme += to_string(getSecondTerm(terme))
elif isAbstraction(getSecondTerm(terme)):
deuxieme_terme += "("+to_string(getSecondTerm(terme))+")"
elif isApplication(getSecondTerm(terme)):
deuxieme_terme += "("+to_string(getSecondTerm(terme))+")"
return premier_terme + ' ' + deuxieme_terme
def to_string(terme):
if isVariable(terme):
return to_string_var(terme)
elif isAbstraction(terme):
return to_string_abs(terme)
return to_string_app(terme)
counters = 0
def counter():
global counters
counters += 1
return counters
def annotate_beta_reduction(terme):
if isVariable(terme): return None
elif isAbstraction(terme):
x = getInputFromAbs(terme)
A = getOutputFromAbs(terme)
B = beta_reduction(A)
if B != None:
return new_abs(x,annotate_beta_reduction(A))
else:
return None
elif isApplication(terme):
A1 = getFirstTerm(terme)
B1 = getSecondTerm(terme)
A2 = beta_reduction(A1)
B2 = beta_reduction(B1)
if isAbstraction(A1):
if A2 != None and B2 != None:
x1 = getInputFromAbs(A1)
C = getOutputFromAbs(A1)
communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
if communBoundVars == []:
return new_app(annotate_beta_reduction(A1),annotate_beta_reduction(B1)) + [substitute(x1,B1,C)] + [counter()]
else:
t=A1
for var in communBoundVars:
t=alpha_rename(t,(var))
return new_app(annotate_beta_reduction(A1),annotate_beta_reduction(B1)) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
if A2 != None and B2 == None:
x1 = getInputFromAbs(A1)
C = getOutputFromAbs(A1)
communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
if communBoundVars == []:
return new_app(annotate_beta_reduction(A1),B1) + [substitute(x1,B1,C)] + [counter()]
else:
t=A1
for var in communBoundVars:
t=alpha_rename(t,(var))
return new_app(annotate_beta_reduction(A1),B1) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
if A2 == None and B2 != None:
x1 = getInputFromAbs(A1)
C = getOutputFromAbs(A1)
communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
if communBoundVars == []:
return new_app(A1,annotate_beta_reduction(B1)) + [substitute(x1,B1,C)] + [counter()]
else:
t=A1
for var in communBoundVars:
t=alpha_rename(t,(var))
return new_app(A1,annotate_beta_reduction(B1)) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
else:
x1 = getInputFromAbs(A1)
C = getOutputFromAbs(A1)
communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
if communBoundVars == []:
return new_app(A1,B1) + [substitute(x1,B1,C)] + [counter()]
else:
t=A1
for var in communBoundVars:
t=alpha_rename(t,(var))
return new_app(A1,B1) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
else:
if A2 != None and B2 != None:
return new_app(annotate_beta_reduction(A1),annotate_beta_reduction(B1))
if A2 != None and B2 == None:
return new_app(annotate_beta_reduction(A1),B1)
if A2 == None and B2 != None:
return new_app(A1,annotate_beta_reduction(B1))
if A2 == None and B2 == None:
return None
def annotated_to_string(terme):
String_term=''
if len(terme)==5:
first=getFirstTerm(terme)
second=getSecondTerm(terme)
String_term+="(\u03BB"+str(terme[4])+to_string(getInputFromAbs(first))+"."+annotated_to_string(getOutputFromAbs(first))+') '
String_term+='('+ annotated_to_string(second)+ ')'
else:
if isApplication(terme):
first=getFirstTerm(terme)
second=getSecondTerm(terme)
String_term+='(' + annotated_to_string(first) + ') '
String_term+= '('+ annotated_to_string(second) + ') '
elif isAbstraction(terme):
String_term+='\u03BB'+ to_string(getInputFromAbs(terme))+ '.' +annotated_to_string(getOutputFromAbs(terme))
else:
String_term+=to_string(terme)
return String_term
def beta_reduction_choice_n(terme,n):
if isVariable(terme): return None
elif isAbstraction(terme):
A = getOutputFromAbs(terme)
B = beta_reduction_choice_n(A,n)
if B != None:
return new_abs(getInputFromAbs(terme), beta_reduction_choice_n((A),n))
else:
return None
elif isApplication(terme):
if len(terme) == 5:
if terme[4] == n:
return terme[3]
else:
terme = terme[:3]
A1 = getFirstTerm(terme)
B1 = getSecondTerm(terme)
A2 = beta_reduction_choice_n(A1,n)
B2 = beta_reduction_choice_n(B1,n)
if A2 != None and B2 != None:
return new_app(beta_reduction_choice_n(A1,n),beta_reduction_choice_n(B1,n))
if A2 != None and B2 == None:
return new_app(beta_reduction_choice_n(A1,n),B1)
if A2 == None and B2 != None:
return new_app(A1,beta_reduction_choice_n(B1,n))
if A2 == None and B2 == None:
return None
else:
terme = terme[:3]
A1 = getFirstTerm(terme)
B1 = getSecondTerm(terme)
A2 = beta_reduction_choice_n(A1,n)
B2 = beta_reduction_choice_n(B1,n)
if A2 != None and B2 != None:
return new_app(beta_reduction_choice_n(A1,n),beta_reduction_choice_n(B1,n))
if A2 != None and B2 == None:
return new_app(beta_reduction_choice_n(A1,n),B1)
if A2 == None and B2 != None:
return new_app(A1,beta_reduction_choice_n(B1,n))
if A2 == None and B2 == None:
return None
def beta_reduction_interactive(terme, at):
global counters
if at != None:
print(annotated_to_string(at))
choice = int(input("Choose a beta reduction: "))
while choice <= 0 or choice > counters:
print("Invalid choice")
choice = int(input("Choose a beta reduction: "))
try:
return beta_reduction_choice_n(at,choice)
finally:
counters = 0
else:
try:
return terme
finally:
counters = 0
def cleanReductions(l):
if isinstance(l, list):
return [cleanReductions(i) for i in l][:3]
else:
return l
def beta_reduction_interactive_totale(terme):
if beta_reduction((terme)) != None:
print(to_string(terme))
at = (annotate_beta_reduction((terme)))
captureImage(at)
choix=int(input("voulez-vous faire la reduction tapez sur 1 pour oui tapez sur 2 pour non "))
if choix==1:
return beta_reduction_interactive_totale(beta_reduction_interactive(terme,at))
else:
terme = cleanReductions(terme)
captureImage((terme))
print("C'est fini, le terme obtenu est : "+to_string(terme))
else:
captureImage(terme)
return (terme)