fun/halting_problem.bruijn


:import std/Logic .

# hypothetical halting decider (shall not loop)
# assuming (Program Arg) reduces to boolean
halting [[halts (1 0)]] ⧗ Program → Arg → Boolean
	halts [0 true false]

# basically y combinator
# paradox!
e halting [¬(halting 0 0)] [¬(halting 0 0)]