What is the relationship between algorithms and logic?

Question

Is an algorithm (cooking a dish, Grover's/Shor algorithm, etc.) a form of deductive reasoning or inductive reasoning, and if not what exactly is the relationship between an alogorithm and logic?

Answer 1

It is neither. A proof that an algorithm solves the problem (it claims to solve) is typically deductive in computer science, but in AI it's more likely to be inductive, i.e. based on benchmarks/experiments.

As for cooking a dish, it depends what you think the problem to be solved is, I suppose. In trivial terms, one can say it's "making food" QED. On the other hand, if the goal of the recipe is to make some specific thing, you'd have to agree to a definition of what that is because you can even discuss proof. Alas, most things in cuisine have subjective or "definition by committee" kind of thing, so it's not really easy to discuss such matters in formal logic.

In the absence of a separate definition for the problem, any algorithm "does what it does", so it's circular logic at best. It is sometimes interesting to ask the question in reverse, i.e. starting from an artifact what does it do, but this seldom done for algorithms in theoretical contexts (as far as I know), but much more often for concrete code, typically for malware analysis etc.

---

I didn't really want to get into this, but since someone posted a rather misleading answer... The Curry Howard correspondence (aka "program as proofs") is commonly misunderstood.

It relates some programming languages (PL) to an intuitionist/constructivist kind of logic. It nether covers all forms of program nor all forms of logic in a meaningful way. A relevant slide form a "for dummies" presentation on that

It's sometimes said that "The logic for a Turing-complete functional language is inconsistent." This is true in the sense explained here. To make the PL Turing-complete you need the Y-combinator (or equivalent). And since that "doesn't type", you either end up with a trivial logic (one type — that's like saying all it can prove is that "a program is a program") or one that is inconsistent, i.e. it can "prove anything is true". To quote from there:

Allowing for non-halting programs is what makes Turing Machines powerful, and is at the heart of the Church-Turing thesis. But as soon as you allow that, any meaningful relation to logic is lost.

So, rewind that here, something like a cooking recipe, since it usually doesn't need to be expressed in a Turing-complete language, is actually more like steps in a logic proof.

That quote above somewhat overstates things, to be honest, but it is true in the sense that CH corresp. isn't useful in the most general case. I had mentioned earlier reverse-engineering "what a program does". That actually is related to how proofs of algorithm correctness works to some extent, if you look at determining pre-conditions and postconditions for a loop in Hoare Logic for instance. But the latter has both proofs and programs part of its derivation scheme, it's not programs as proofs.

Regarding Curry-Howard, you could (roughly) say that a (guaranteed) terminating program/algorithm provides its "own proof" of what it does. But you have to think carefully what that statement means in terms of our understanding. It's not really different to saying "a program does what it does" until you identify a type system that is "insightful enough" to give you an alternative explanation for "what it does".

N.B. as far as theoretical CS research, you could say Hoare Logic has been recast as Hoare Type Theory, which is more or less the same thing as using lax logic (a kind of modal logic) to represent monands. One of the papers in this area has a philosophically intersting quote:

It is usually said that a constructive proof is a program. However, exactly speaking, we should say that a constructive proof consists of a program and its correctness proof. The correctness part is not necessary at runtime. The realizability interpretation cuts off the correctness part (to some extent) and extracts the program part. When we describe the specification of a program or prove a certain theorem in modal logic, we need the \nec-modality in general, because \nec\ is needed for correctness proofs. However, the comonad types that model \nec-modality are not necessarily needed in the type system for the extracted programs, because “the correctness part” is no longer needed.

So, yeah, amusingly, one can use the CH correspondence (in a broad sense) to sort-of prove that correctness proofs are somewhat independent from the underlying programs/algorithms, at least for "imperative recipes" that manipulate a stateful world.

Answer 2

Algorithms are more closely related to deductive reasoning, but it's not quite as straightforward as that. Suppose for simplicity that by deductive reasoning, you roughly mean a proof given in a logic of your choice, and that by algorithm, you roughly mean Turing machine, lambda calculus, or some other equivalent formalization of computation.

Then, in a large class of cases, deductive reasoning can be captured by an algorithm. Consider any instance of deductive reasoning, that is, a proof: a sequence of propositions, each of which meets certain nice properties. We say that such a sequence is a proof of its last sentence. Given that the logic in question is suitably nice - say recursively axiomatizable, we can implement an algorithm to check that such a sequence is really a proof. Of course, even nicer logics can give us more than that — given a set of assumptions, we might find an algorithm that enumerates every consequence of those assumptions. Further, by Curry Howard, we can actually view proofs as programs (in a suitably expressive language). So deductive reasoning might be seen as a form of computation, instead.

Answer 3

Simply put, according the Curry-Howard isomorphism a program is an isomorphism to a logical proof. From WP:

[T]he Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.

Why is that so? A simple example might help explain.

$a:=2;
$b:=20;
$c:=Summation($a,$b); -- Add the number 2 20 times.
print $c;
:40

There are two ways at looking at the pseudo code. First, you can view the first line as an imperative to execute as part of an algorithm. While this program is simple, and merely takes two inputs and executes repeated addition, it's a simple implementation of repetitive addition, that is a simple algorithm. From WP:

In mathematics and computer science, an algorithm (/ˈælɡərɪðəm/ (listen)) is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation.

But on the other hand, you can view each line as a statement of logical truth. Let's rewrite:

Premise 1: The variable a has a value of 2.
Premise 2: The variable b has a value of 20.
Conclusion: The summation of a b times is 40.

Now, in logic, we'd say, how do we know the conclusion is true? Of course, we'd can show the inference is correct by skip-counting from 2 to 40. And if really wanted to get rigorous, we can rewrite the entire proof in Peano's system and show the formal system is deductively valid. But is there a fundamental difference between the logical approach and the mathematical approach that we automate with a computer? Nope! What differs only is the context.

For simplicity, I've taken an arithmetic problem and shown it's relationship to deduction. Can the same be done with induction or abduction? Sure. If one institutes a statistical algorithm that leads to a confidence interval, for instance, then one is now using inductive logic since an induction is an inference where the conclusion doesn't necessarily follow from the presmises.

Should all of this be surprising? Perhaps, but note that the inventor of the formal system, Gottlob Frege, who also invented modern formalisms of logic was, along with David Hilbert, roughly put trying to show that there was an objective basis for mathematical truth by trying to reduce mathematics to logic. Since computers are essentially machines that automate mathematics along with logic, an algorithm is essentially a proof that can use any logic. (And yes, there are a large number of logics and methods of inference of which deduction, induction, and abduction are atoms.)

Answer 4

Algorithms are time-bound sets of instructions. Logic is an atemporal transfer of properties among classes and their instances.

A logical proof (in principle) takes no time and makes no changes. The final result or conclusion is implicit within the original premises, and in fact says nothing that was not contained in the original premises. An algorithm makes progressive changes to the original material, ultimately creating something new that is not reducible to the original material.

We can talk about the process of 'doing logic' as an algorithm, where we progressively modify our original premises to produce something that appears to be new. But ultimately logic doesn't need 'time in the oven' (the way baking a cake does). It's not an act of creation, but an act of exposing what was already present.

Answer 5

Logic is the formal expression of the rules of reason.

An algorithm is a process, which must be based on logic in order to be useful for an individual or a computer.

An algorithm is not "a form of deductive or inductive reasoning".

Answer 6

What exactly is the relationship between an algorithm and logic?

Dictionary definition:

Algorithm: A finite set of unambiguous instructions that, given some set of initial conditions, can be performed in a prescribed sequence to achieve a certain goal and that has a recognizable set of end conditions.

An algorithm is fundamentally a set of instructions (in some language).

You use your innate logical faculty to be able to conceive, understand or apply algorithms, in the same way that you use your innate logical faculty to be able to understand how things in the world work, to conceive, design or build machines that work, or to use machines to make them work, including computers, which are machines which like all machines humans design in such a way as to be able to use them.

Computers are machines and as such essentially physical processes. There is no logic within physical processes outside animal brains. The logic that we see in natural processes is the logic of our own brain as we try to understand these processes. The logic we see in computers is really the logic inside our own brain. There is no logic inside computers.