Readit News- McCarthy's "Direct Union" is probably conflating "disjoint union" and "direct sum".
- ML probably got the sum/product names from Dana Scott's work. It's unclear if Scott knew of McCarthy's paper or was inspired by it.
- I called ALGOL-68 a "curious dead end" but that's not true: Dennis Ritchie said that he was inspired by 68 when developing C. Also, 68 had exhaustive pattern matching earlier than ML.
- Hoare cites McCarthy in an earlier version of his record paper [2].
Also I kinda mixed up the words for "tagged unions" and "labeled unions". Hope that didn't confuse anybody!
[1] https://lobste.rs/s/ppm44i/very_early_history_algebraic_data...
I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips
My understanding is that solvers are like regexes. They can easily get out of hand in runtime complexity. At least this is what I have experienced from iOS's AutoLayout solver
from z3 import \*
a, b, c = Ints('a b c')
x, y = Ints('x y')
s = Solver()
s.add(a > 5)
s.add(a % 2 == 0)
theorem = Exists([b, c],
And(
a == b + c,
And(
Not(Exists([x, y], And(x > 1, y > 1, x \* y == b))),
Not(Exists([x, y], And(x > 1, y > 1, x \* y == c))),
)
)
)
if s.check(Not(theorem)) == sat:
print(f"Counterexample: {s.model()}")
else:
print("Theorem true")That said, I don't think OP's antics are a crime. That SyntaxError though, that might be a crime.
And a class-generating callable class would get around Python caching the results of __subclasshook__.
- T550.6. T550.6. Only half a son is born by queen who ate merely half of mango.
- A1066. A1066. Sun will lock moon in deep ditch in earth's bottom and will eat up stars at end of world.
- K87.1. K87.1. Laughing contest: dead horse winner.
I fail to see how you validate that TLA+ model is actually correctly mapped into the written Java code.
[0] https://cdn.aaai.org/ICAPS/2005/ICAPS05-027.pdf