LVM 2: Boolean Writup ============================= ``` The original lambda expression is like:
(λ ABCDEF GHIJKL | (#≃ A #.) ((#≠ B #?) #𝐅 (...)) #𝐅)
Define macro:
.l(𝐬) (λxyz|y(xyz)) -> successor
.l(𝐓) (λxy|x) -> true
.l(𝐅) (λxy|y) -> false
.l(¬) (λw|w#𝐅#𝐓) -> not
.l(ζ) (λx|x #𝐅 #¬ #𝐅) -> zerop
.l(𝐩) (λxsz|x(λgh|h(gs))(λu|z)(λu|u)) -> predecessor
.l(∸) (λxy|y#𝐩x) -> monus subtraction
.l(∧) (λwz|wz#𝐅) -> and
.l(≃) (λab|(#∧(#ζ(#∸ab))(#ζ(#∸ba)))) -> equalp
.l(≠) (λjk|#¬(#≃jk)) -> neq_p
.l(+) (λxy|y#𝐬x) -> addition
.l(×) (λxys|x(ys)) -> multiplication
It is generated by Python code, see `2.py’ for details.
But it should notice that the given lambda expression is not computed in the ABCDEFGHIJKL sequence, you can reorder the original lambda expression like:
(λKCJIHEBLADGF|...)
copy the lambda calculus function body and save it as a Python string:
expr = "(λw|w(λxy|y)(λxy|..."
you can get the variable by its appearance:
''.join(re.compile("[A-Z]").findall(expr))
# => KCJIHEBLADGF
Think it is not strict (general) enough? Sure, you could take use of the AST by:
from parse import parse
expr_ast = parse("...") # the function
def search(ast : AST, depth : int = 0) -> None:
if ast.terminate_p() and re.match("[A-Z]", ast.root):
print(f"{ast}: {depth}")
elif ast.application_p():
search(ast.fn_expr(), depth + 1)
search(ast.arg_expr(), depth + 1)
elif ast.function_p():
search(ast.fn_body(), depth + 1)
So change the `task-2-lambda-expr’ like this:
.l(f) \ -> set the secret lambda function expression
(λK|(λC|(λJ|(λI|(λH|(λE|(λB|(λL|(λA|(λD|(λG|(λF|((((λw|((w(λ\
x|(λy|y)))(λx|(λy|x))))(((λa|(λb|(((λw|(λz|((wz)(λx|(λy|y)))\
Or, you can construct a reorder function like below:
.l(r) (λfKCJIHEBLADGF|fABCDEFGHIJKL)
so the original f could be used as:
.l(g) #r #f
now you can crack it one by one in sequence.
If you’ve followed the tips, you may found out that:
| .l(t) (λAB | (#≃A#1)((#≃B#2)#𝐓#𝐅)#𝐅) | |||||||||||||||||||||||
| #t #1 #2 -> (λxy | x) | |||||||||||||||||||||||
| #t #2 -> (λBxy | y) | |||||||||||||||||||||||
| #t #1 -> (λB | B(λgh | h(g(λgh | h(g(λxy | y)))))(λu | (λuw | w(λxy | y)(λxy | x)))(λu | u)(λu | u)(λxy | y)(B(λxsz | x(λgh | h(gs))(λu | z)(λu | u))(λsz | s(sz))(λxy | y)(λw | w(λxy | y)(λxy | x))(λxy | y))(λxy | y)(λxy | x)(λxy | y)) |
samely, you can test the task lambda expr one by one:
#f #1 -> (λCJIHEBLADGFxy|y) #f #2 -> (λCJIHEBLADGFxy|y) … #f #8 -> (λCJIHEBLADGF|C(λxsz|x(λgh|h(gs))(λu|z)(λu|u))(λya|y(y(y(y(y(y(y(y(y(y(y(y(ya))))))))))… so the “first” K is 8 -> `h’.
since trying each bit is a little slow, it is wiser to write a program and try checking it every time.
a lazy way to do this is like:
from utils import AST from parse import parse from compute import compute from lvm_repl import make_church_number expr_ast = parse(“…”) # the task lambda expr syms = “KCJIHEBLADGF” flag = [char for char in “****”] ast = expr_ast for j in syms: max_len, max_i, max_res = 0, 0, None for i in range(26): res = compute(AST(“←”, ast, make_church_number(i + 1)), 512) if len(str(res)) > max_len: max_len, max_i, max_res = len(str(res)), i, res ast, flag[ord(j) - ord(“A”)] = max_res, chr(max_i + ord(“a”))
’‘.join(flag) # => lambdaknight
So the flag is `ucatflags{lambdaknight}’.
see `2-solve.py’ for a more complete and general code to do such thing.
Do you have other method to solve this problem? (of cource there should be other ways, for example, reduce the lambda expression by hand, or use other brute force to guess.).
Quote: さてどこへ行こうかしらね、ネットは広大だわ 草薙素子
P.S. do you know lambda knight?
`2-solve.py`
```python
from lib.utils import AST
from lib.parse import parse
from lib.compute import compute
from lvm_repl import make_church_number
import re
expr_ast = parse("(λA|(λB|(λC|(λD|(λE|(λF|(λG|(λH|(λI|(λJ|(λK|(λL|((((λw|((w(λ" + \
"x|(λy|y)))(λx|(λy|x))))(((λa|(λb|(((λw|(λz|((wz)(λx|(λy|y)))" + \
"))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|" + \
"(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|" + \
"z))(λu|u))))))x)))a)b)))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|" + \
"y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x" + \
"(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))b)a)))))((λb|(((λx|(" + \
"λy|((y(λx|(λy|(λz|(y((xy)z))))))x)))(((λx|(λy|(λs|(x(ys)))))" + \
"b)(λs|(λz|(sz)))))(λs|(λz|(s(s(sz)))))))(λs|(λz|(s(s(s(s(sz)" + \
"))))))))K))(λx|(λy|y)))((((λw|((w(λx|(λy|y)))(λx|(λy|x))))((" + \
"(λa|(λb|(((λw|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λ" + \
"w|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx" + \
"|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))(" + \
"(λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy" + \
"|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))" + \
"(λu|u))))))x)))b)a)))))((λb|(((λx|(λy|((y(λx|(λy|(λz|(y((xy)" + \
"z))))))x)))(((λx|(λy|(λs|(x(ys)))))b)(λs|(λz|(sz)))))(λs|(λz" + \
"|(s(s(s(sz))))))))(λs|(λz|(s(s(s(s(s(s(s(s(sz)))))))))))))C)" + \
")(λx|(λy|y)))((((λw|((w(λx|(λy|y)))(λx|(λy|x))))(((λa|(λb|((" + \
"(λw|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(" + \
"λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(" + \
"((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((x(λ" + \
"x|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λ" + \
"x|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u)))))" + \
")x)))b)a)))))((λb|(λs|(λz|(s(s(s(s(s(s(sz))))))))))(λs|(λz|(" + \
"s(s(s(s(s(s(s(s(sz)))))))))))))J))(λx|(λy|y)))(((((λa|(λb|((" + \
"(λw|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(" + \
"λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(" + \
"((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((x(λ" + \
"x|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λ" + \
"x|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u)))))" + \
")x)))b)a)))))((λb|(((λx|(λy|((y(λx|(λy|(λz|(y((xy)z))))))x))" + \
")(λs|(λz|(s(s(sz))))))(((λx|(λy|(λs|(x(ys)))))b)(λs|(λz|(sz)" + \
")))))(λs|(λz|(s(s(s(s(s(sz))))))))))I)(((((λa|(λb|(((λw|(λz|" + \
"((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(" + \
"λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(" + \
"λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((x(λx|(λy|y)" + \
"))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((" + \
"y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))b)a" + \
")))))((λb|(((λx|(λy|((y(λx|(λy|(λz|(y((xy)z))))))x)))(((λx|(" + \
"λy|(λs|(x(ys)))))b)(((λx|(λy|((y(λx|(λy|(λz|(y((xy)z))))))x)" + \
"))(λs|(λz|(sz))))(((λx|(λy|(λs|(x(ys)))))b)(λs|(λz|(sz))))))" + \
")(λs|(λz|(s(sz))))))(λs|(λz|(s(s(sz)))))))H)(((((λa|(λb|(((λ" + \
"w|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy" + \
"|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((" + \
"x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((x(λx|" + \
"(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|" + \
"(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x" + \
")))b)a)))))((λb|(λs|(λz|(s(s(s(sz)))))))(λs|(λz|(s(s(s(s(s(s" + \
"(sz)))))))))))E)((((λw|((w(λx|(λy|y)))(λx|(λy|x))))(((λa|(λb" + \
"|(((λw|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λ" + \
"x|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λ" + \
"z|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((" + \
"x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(" + \
"((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))" + \
"))))x)))b)a)))))((λb|(λs|(λz|(sz))))(λs|(λz|(s(s(s(sz)))))))" + \
")B))(λx|(λy|y)))(((((λa|(λb|(((λw|(λz|((wz)(λx|(λy|y)))))((λ" + \
"x|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y" + \
"))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λ" + \
"u|u))))))x)))a)b)))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(" + \
"λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(" + \
"λh|(h(gs)))))(λu|z))(λu|u))))))x)))b)a)))))((λb|(((λx|(λy|((" + \
"y(λx|(λy|(λz|(y((xy)z))))))x)))(((λx|(λy|(λs|(x(ys)))))b)(λs" + \
"|(λz|(s(s(sz)))))))(λs|(λz|(s(sz))))))(λs|(λz|(s(s(s(s(s(sz)" + \
")))))))))L)((((λw|((w(λx|(λy|y)))(λx|(λy|x))))(((λa|(λb|(((λ" + \
"w|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy" + \
"|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((" + \
"x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((x(λx|" + \
"(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|" + \
"(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x" + \
")))b)a)))))((λb|(((λx|(λy|((y(λx|(λy|(λz|(y((xy)z))))))x)))(" + \
"((λx|(λy|(λs|(x(ys)))))b)(λs|(λz|(s(sz))))))(λs|(λz|z))))(λs" + \
"|(λz|(s(s(s(s(s(sz))))))))))A))(λx|(λy|y)))(((((λa|(λb|(((λw" + \
"|(λz|((wz)(λx|(λy|y)))))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|" + \
"y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x" + \
"(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))a)b)))((λx|(((x(λx|(" + \
"λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y))))(((λx|(" + \
"λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λu|u))))))x)" + \
"))b)a)))))((λb|(λs|(λz|(s(sz)))))(λs|(λz|(s(s(s(s(s(s(s(s(s(" + \
"sz))))))))))))))D)(((((λa|(λb|(((λw|(λz|((wz)(λx|(λy|y)))))(" + \
"(λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy" + \
"|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))" + \
"(λu|u))))))x)))a)b)))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y))" + \
")(λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg" + \
"|(λh|(h(gs)))))(λu|z))(λu|u))))))x)))b)a)))))((λb|(((λx|(λy|" + \
"((y(λx|(λy|(λz|(y((xy)z))))))x)))(((λx|(λy|(λs|(x(ys)))))b)(" + \
"λs|(λz|(sz)))))(λs|(λz|(sz)))))(λs|(λz|(s(s(s(s(s(s(s(s(s(sz" + \
"))))))))))))))G)(((((λa|(λb|(((λw|(λz|((wz)(λx|(λy|y)))))((λ" + \
"x|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(λx|(λy|x)))))(λx|(λy|y" + \
"))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(λh|(h(gs)))))(λu|z))(λ" + \
"u|u))))))x)))a)b)))((λx|(((x(λx|(λy|y)))(λw|((w(λx|(λy|y)))(" + \
"λx|(λy|x)))))(λx|(λy|y))))(((λx|(λy|((y(λx|(λs|(λz|(((x(λg|(" + \
"λh|(h(gs)))))(λu|z))(λu|u))))))x)))b)a)))))((λb|(λs|(λz|(sz)" + \
")))(λs|(λz|(s(s(s(sz))))))))F)(λx|(λy|x)))(λx|(λy|y))))(λx|(" + \
"λy|y))))(λx|(λy|y)))))(λx|(λy|y)))))(λx|(λy|y))))(λx|(λy|y))" + \
"))(λx|(λy|y))))))))))))))))))") # the task lambda expr
# if you use stdin for input expr ast
# expr_ast = parse(input())
syms = []
def search(ast : AST) -> None:
if ast.terminate_p() and re.match("[A-Z]", ast.root):
syms.append(ast.root)
elif ast.application_p():
search(ast.fn_expr())
search(ast.arg_expr())
elif ast.function_p():
search(ast.fn_body())
search(expr_ast)
print(f"sym sequence: {''.join(syms)}")
def reorder_fn_ast(order : list) -> AST:
"""
(λFabcdefg|Fgfedcba) #F -> reorder the argument
"""
in_order = [AST(chr(i + ord("A"))) for i in range(len(order))]
ast = AST("f")
for sym in in_order:
ast = AST("←", ast, sym)
for sym in reversed(order):
ast = AST("λ", AST(sym), ast)
return AST("λ", AST("f"), ast)
reorder_ast = reorder_fn_ast(syms)
print("reordered:", reorder_ast.prettify())
flag = [char for char in "************"]
ast = AST("←", reorder_ast, expr_ast)
for j in syms:
max_len, max_i, max_res = 0, 0, None
for i in range(26):
res = compute(AST("←", ast, make_church_number(i + 1)), 512)
if len(str(res)) > max_len:
max_len, max_i, max_res = len(str(res)), i, res
elif len(str(res)) == max_len and max_len != 0:
res = compute(AST("←", AST("←", res, AST("t")), AST("f")), 512)
if res.terminate_p() and res.root == "t":
max_i = i
break
ast, flag[ord(j) - ord("A")] = max_res, chr(max_i + ord("a"))
print(f"flag: {''.join(flag)}")
print(''.join(flag))