How do algorithms solve real world problems if they work
without referring to the meanings of the symbols? Algorithms are a form of
logic. It is possible to use algorithms to make logical inferences about the
data. Well chosen logical inferences can solve practical problems.
This use
of algorithms requires the programmer to define an additional set of conventions
about data types. Consider the following series of statements.
- "Abraham
Lincoln" is a character string.
- "Abraham Lincoln" is the name of a human
being.
- "Abraham Lincoln" is the name of a politician.
- "Abraham Lincoln"
is the name of a president of the United States of America.
Each of them
is attaching a data type to the character string "Abraham Lincoln". Most
computer languages are only concerned with the data type in line 1. This is all
they need to generate executable code. But logicians have been interested in
more elaborate forms of data typing. Each of the statements mentions a valid
data type in this logical sense. Logicians have noticed that data types
corresponds to what they call "predicates" which are templates to form
propositions. For example "is the name of a president of the USA" is a
predicate. If you apply it to "Abraham Lincoln" you are stating the (true)
proposition that "Abraham Lincoln" is the name of a president of the USA. And if
you attach the same predicate to "Albert Einstein" you get a similar but false
proposition.
When writing a program, programmers must first define their
data. They don't just define the syntactic representation in terms of bits. They
also define what the data will mean. A logician would say they define the
logical data types, the predicates which are associated with the data. These
predicates are documented in the specifications of the software, in comments
included in the source code or in the names they give to the program variables.
This knowledge is essential in understanding a program. However these predicates
are not used for generating machine executable instructions. The predicates are
not used by the computer for the manipulation of the symbols. During execution
the predicates are implicit. They are defined by a convention the reader must
know in order to be able to read the symbols correctly. They are for human
understanding and verification that the program indeed does what it is intended
to do. And they are also for the user of the program as he needs to understand
the meanings of the inputs and outputs in order to use the program
properly.
Data types in this extended logical sense relate to algorithms as
follows. If you expect the data to be of some type, then the data is implicitly
stating a proposition. You can tell which proposition by applying the predicate
to the data. If you expect a quantity of hammers in your inventory and the data
you get is 6, then you implicitly have a statement that you currently have 6
hammers in stock. All data is implicitly the statement of a proposition
corresponding to its type.
When the algorithm process the data it implicitly
carries out logical inferences on the corresponding propositions because a
correctly working program must always produce data of the correct type. For
example if you ask a program for the birth date of Theodore Roosevelt and the
program returns October 27, 1858, it implicitly states that this is the birth
date of Theodore Roosevelt because this is the proposition corresponding to the
expected data type. The definition of correctness for a program is that it
produces a logically correct answer. Programmers are well aware of this
correspondence between predicates, data and correctness. They use it to design,
understand and verify their programs.
Logicians have defined a
mathematically rigorous correspondence between algorithms and mathematical
logic. This is called the Curry-Howard correspondence. It works like a
translation, similar to translating between Russian and Chinese, except that the
translation is between two mathematical languages. If the algorithm is expressed
in the language of λ-calculus then the Curry-Howard correspondence
translates the algorithm into a proof of mathematical logic expressed in the
language of predicate calculus. The translation works also in the other
direction. Proofs of mathematical logic may likewise be translated into
algorithms. In this sense an algorithm is really another expression for rules of
logic. The difference is a matter of form and not substance.
As an
alternative, when the algorithm is written in an imperative language instead of
λ-calculus it may be assigned a logical semantics using Hoare logic.
Poernomo, Crossley and Wirsing argue that Hoare logic is what the Curry-Howard
correspondence becomes when it is adapted to imperative
programs.
I have some questions for you. Is logic useful? Why
would putting operations of logic in a computer make them patentable?
In my
opinion, the utility of a stored program computer is analogous to the utility of
a printing press. It does not depend on the contents. There is a mathematical
basis to the notion that an algorithm is a form of logic. Also there is a
technological basis to the notion that the hardware is independent from the
contents. Perhaps this address your question?
