August 12, 2014
On Sunday, 10 August 2014 at 02:40:31 UTC, Ola Fosheim Grøstad wrote:
> Of course it does, that is why Hoare Logic and SSA exist. Deduction lacks a notion of time.

Logic is ordered, and we have a notion of order because we know time, which is the only obviously ordered thing in nature. So in a sense any logic has time in its foundation and math can do the reverse: represent time in declarative manner.
August 12, 2014
On Tuesday, 12 August 2014 at 04:50:15 UTC, Kagamin wrote:
> Logic is ordered, and we have a notion of order because we know time, which is the only obviously ordered thing in nature. So in a sense any logic has time in its foundation and math can do the reverse: represent time in declarative manner.

No, there is no order to boolean expressions. Deduction can be
performed bottom up. Imperative programs rely on top down
execution due to side effects.

Recall that all pure functions over finite types can be implemented as tables. A table lookup is O(1). No time.
August 12, 2014
On Tuesday, 12 August 2014 at 05:47:22 UTC, Ola Fosheim Grøstad wrote:
> On Tuesday, 12 August 2014 at 04:50:15 UTC, Kagamin wrote:
>> Logic is ordered, and we have a notion of order because we know time, which is the only obviously ordered thing in nature. So in a sense any logic has time in its foundation and math can do the reverse: represent time in declarative manner.
>
> No, there is no order to boolean expressions. Deduction can be
> performed bottom up.

A true reversal would be when preconditions are derived from postconditions.

> Recall that all pure functions over finite types can be implemented as tables. A table lookup is O(1). No time.

That's different logic, and algorithmic complexity is time.
August 12, 2014
On Tuesday, 12 August 2014 at 08:07:01 UTC, Kagamin wrote:
> A true reversal would be when preconditions are derived from postconditions.

That's how you conduct a proof…

>> Recall that all pure functions over finite types can be implemented as tables. A table lookup is O(1). No time.
>
> That's different logic, and algorithmic complexity is time.

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…
August 12, 2014
On Tuesday, 12 August 2014 at 09:17:54 UTC, Ola Fosheim Grøstad wrote:
> On Tuesday, 12 August 2014 at 08:07:01 UTC, Kagamin wrote:
>> A true reversal would be when preconditions are derived from postconditions.
>
> That's how you conduct a proof…

A proof usually flows from causes to consequences, the reverse (induction) is ambiguous. Ordering is more fundamental: you can define or redefine it, but it will remain, one can't think outside of this formalism.

> 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.
August 13, 2014
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.
12 13 14 15 16 17 18 19 20 21 22
Next ›   Last »