bernatbc / lambda-calculus-telegram-bot Goto Github PK

Rename conflicitve variables, for example:
λx.λx.y -> λx.λz.y

Symbols like ',' make an error.
For example 'N2 , N2' works while 'N2,N2' doesn't.

Alpha-conversion is not correct

Checking string value to know if we should stop recursion.

There're graph image limit, as well sometimes there's a time limit exception

When input is
N2≡λs.λz.s(s(z))
N3≡λs.λz.s(s(s(z)))
N2 N3
it outputs
(λz.(λz.(((z(z(zz)))((z(z(zz)))((z(z(zz)))(z(z(zz))))))(((z(z(zz)))((z(z(zz)))((z(z(zz)))(z(z(zz))))))(((z(z(zz)))((z(z(zz)))((z(z(zz)))(z(z(zz))))))((z(z(zz)))((z(z(zz)))((z(z(zz)))(z(z(zz)))))))))))

but it should output

λz.λz1.z(z(z(z(z(z(z(z(zz1))))))))

Add more symbols in infix macros

Should print only the sub-tree where an alpha-conversion is required. Currently it prints the whole tree.

En aquesta tasca heu de permetre la definició de macros amb notació infixa. En aquests cas els noms seran símbols no alfabètics i la seva implementació serà similar a les macros amb notació prefixa. Veieu l’exemple següent:
`
? N2≡λs.λz.s(s(z))
N2 ≡ (λs.(λz.(s(sz))))
? N3≡λs.λz.s(s(s(z)))
N2 ≡ (λs.(λz.(s(sz))))
N3 ≡ (λs.(λz.(s(s(sz)))))
? +≡λp.λq.λx.λy.(px(qxy))
N2 ≡ (λs.(λz.(s(sz))))
N3 ≡ (λs.(λz.(s(s(sz)))))

• ≡ (λp.(λq.(λx.(λy.((px)((qx)y))))))
  ? N2+N3
  Arbre:
  (((λp.(λq.(λx.(λy.((px)((qx)y))))))(λs.(λz.(s(sz)))))(λs.(λz.(s(s(sz))))))
  β-reducció:
  ((λp.(λq.(λx.(λy.((px)((qx)y))))))(λs.(λz.(s(sz))))) → (λq.(λx.(λy.(((λs.(λz.(s(sz))))x)((qx)y)))))
  β-reducció:
  ((λq.(λx.(λy.(((λs.(λz.(s(sz))))x)((qx)y)))))(λs.(λz.(s(s(sz)))))) → (λx.(λy.(((λs.(λz.(s(sz))))x)(((λs.(λz.(s(s(sz)))))x)y))))
  β-reducció:
  ((λs.(λz.(s(sz))))x) → (λz.(x(xz)))
  β-reducció:
  ((λz.(x(xz)))(((λs.(λz.(s(s(sz)))))x)y)) → (x(x(((λs.(λz.(s(s(sz)))))x)y)))
  β-reducció:
  ((λs.(λz.(s(s(sz)))))x) → (λz.(x(x(xz))))
  β-reducció:
  ((λz.(x(x(xz))))y) → (x(x(xy)))
  Resultat:
  (λx.(λy.(x(x(x(x(xy)))))))
  `

In the statement: 'La funció ha de tenir un paràmetre que limiti el nombre de reduccions a un màxim per evitar els casos en que les crides recursives no acaben.'

When ending the input, an error of End Of File (EOF) appears.

Return True if a beta-reduction has happened, false otherwise, so we can decide when to stop

When a tree does multiple alpha-conversions, it should print each step of a conversion

Give an option to reduct a macro.
For example:
N18≡ (((λp.(λq.(λx.(λy.((px)((qx)y))))))(((λp.(λq.(λx.(λy.((px)((qx)y))))))(((λp.(λq.(λx.(λy.((px)((qx)y))))))(λs.(λz.(s(s(sz))))))(λs.(λz.(s(s(sz)))))))(((λp.(λq.(λx.(λy.((px)((qx)y))))))(λs.(λz.(s(s(sz))))))(λs.(λz.(s(s(sz))))))))(((λp.(λq.(λx.(λy.((px)((qx)y))))))(λs.(λz.(s(s(sz))))))(λs.(λz.(s(s(sz)))))))
/reduct N18
N18=(λu.(λo.(u(u(u(u(u(u(u(u(u(u(u(u(u(u(u(u(u(uo))))))))))))))))))))

/macros command should show each macro in the system

Output are through terminal instead via telegram

When alpha-conversion runs out of variables, it assigns 'none'. It should assign new variables.

It prints 'Nothing' when a beta-reduction is not needed. It should print its tree.

Once a beta-reduction is found, carry on searching for beta-reductions and replace the while loop in main for a single call.