On Tuesday, 12 August 2014 at 14:43:23 UTC, Kagamin wrote:
A proof usually flows from causes to consequences, the reverse
(induction) is ambiguous.
If a deterministic imperative program is ambigious then there is
something wrong. So no, ambiguity is not the problem. The size if
the search space is. The preconditions are "the ambiguity" which
the theorem prover try to find...
Ordering is more fundamental: you can define or redefine it,
but it will remain, one can't think outside of this formalism.
Explain.
Not at all. You can create a boolean expression for every bit
of output and evaluate it only using NAND gates (or NOR). Not
practical, but doable…
Mathematics is pretty aware of differences between algorithms,
and proving their equivalence is non-trivial.
Define non-trivial. We were talking about the nature of finite
computations. They are all trivial. Algorithms are just
compression of space.
