# What is the relationship between algorithms and logic?

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?

• cooking a dish is not an algorithm but a recipe. The differences are many, but one would be precise vs vague instructions: e.g. "stir calmly for a few minutes" is not algorithmic. Commented Jul 30, 2022 at 8:55
• @csstudent1418 An algorithm is a set of steps to solve a problem or perform a process. A recipe is a type of algorithm. Why isn't "stir calmly for a few minutes" a valid step in the algorithm? It might not be understood by a computer, but it can obviously be followed by a human. Commented Jul 30, 2022 at 16:06
• @csstudent1418 Algorithms have existed for thousands of years before computers. Computer programs are types of algorithms, but they're not equivalent. Wikipedia gives cookiing recipes and bureaucratic processes as other examples of algorithms. Commented Jul 30, 2022 at 16:19
• @csstudent1418 Euclid’s algorithm on two incommensurable line segments has been preformed in theory and practice for thousands of years, an algorithm which can’t be put into Turing tape, according to Yuri Gurevich. web.eecs.umich.edu/~gurevich/Opera/209a.pdf Pg 4 Commented Jul 30, 2022 at 16:32
• Algorithm (dictionary definition): 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. No notion of "computer" here. Commented Jul 30, 2022 at 16:54

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.

• As I see the wiki article on Hoare logic is rather "meh"... besides that it doesn't mention relation to type theory (and lax logic), it also doesn't mention the problem of "biabduction", which is to determine the pre- and post-conditions rather than (a human having to) assert them. Although the latter terminology was introduced in separation logic which also handles pointers (something that Hoare logic doesn't), "biabduction" as notion is not really related to pointers. Commented Jul 30, 2022 at 20:51
• Minor nitpick: An ML model rarely ever "solves" the problem they are used for. You accept some error because otherwise you would have no solution at all (or too costly solution). In fact, I would be very sceptical of any ML model claiming to be perfect (overfitting much?!). Commented Aug 1, 2022 at 5:56

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.

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.)

• The Curry-Howard isomorphism is a mapping between a type theory (programming language) and a logic. Not all programming languages have logically sound type systems. If we take the untyped lambda calculus we have algorithms (programs) but no obvious mapping to logic, since the terms of the calculus all have the same type. Under Curry-Howard this corresponds to a logic with single proposition, which is not exactly what we have in mind by deductive proof. So isn't it more accurate to say that a program together with a suitable type theoretic structure is isomorphic to a proof within a logic? Commented Jul 30, 2022 at 3:37
• @AviC Yes. However, does your anwer make it easier or harder for the OP to understand the relationship? If I had added more information, say the BNF or gone into the details of a type system, would clarity have been gained? Sometimes we sacrifice precision for comprehension, do we not?
– J D
Commented Jul 30, 2022 at 11:42
• The example you gave (with adding the variables a and b) has 99% to do with Hoare logic (preconditions and postconditions) and 1% to do with CH (only via monads as types etc.) Commented Jul 31, 2022 at 0:23
• @JD Your answer was great, and I agree that it is good to keep things simple and straightforward. I raised this in a comments not to dispute your answer but to elaborate on it and clarify it for myself and anybody else who might be interested in diving deeper. I've seen pop philosophers like Joscha Bach misuse Curry-Howard to claim that since all programming languages are Turing complete, therefore all logics are fundamentally equivalent. To see that this is not true, one has to understand that a logic is isomorphic to a programming language together with a type theory of that language. Commented Jul 31, 2022 at 15:19
• @AviC No my answer is not great, and my attacks on your formulation are derivative of the inherent smear your more sophisticated response entails. I should have had more faith in the OP's capacity, and I'll make a second pass that traces the arc from Turing to Brouwer. It's an incisive criticism to call out the conflation between proof and program with proof theory and computational formalisms. I'll take another pass at the advanced undergraduate level.
– J D
Commented Aug 1, 2022 at 4:47

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.

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".

• No down vote, but AI textbooks are encyclopedias of algorithms that formalize reason.
– J D
Commented Jul 30, 2022 at 11:46

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.