do not take natural language too seriously

Freek Wiedijk Radboud University Nijmegen

Seminar Formal Mathematics University of Bonn

2007 04 17, 13:00 programming languages

C:  i++;
Cobol:  ADD 1 TO i.

HyperTalk:

function delimitedSum theList, listDelimiter
put the itemDelimiter into storedDelim -- save itemDelimiter for restore
if listDelim is empty then put comma into listDelimiter -- like 'sum'
else set the itemDelimiter to char 1 of value(listDelimiter) -- UNlike 'sum'
put 0 into sumOfItems
repeat with i = 1 to number of items in theList
  add value(item i of theList) to sumOfItems -- try to convert to a number
end repeat
set the itemDelimiter to storedDelim -- restore itemDelimiter
return sumOfItems
end delimitedSum

making a programming language looks like natural language is a silly idea formulas

solutions of x^{3} + px = q: x^{3} + 6x = 20:

modern style:

\sqrt[3]{\sqrt{108} + 10} − \sqrt[3]{\sqrt{108} − 10} x = \sqrt[3]{\frac{q}{2} ± \sqrt{(\frac{q}{2})^{2} + (\frac{p}{3})^{3}}} − \sqrt[3]{−\frac{q}{2} ± \sqrt{(\frac{q}{2})^{2} + (\frac{p}{3})^{3}}}

ancient style (Gerolamo Cardano, Ars magna, Nürnberg, 1545):

Cube the third part of the number of unknowns, to which you add the square of half the number of the equation, and take the root of the whole, that is, the square root, which you will use, in the one case adding the half of the number which you just multiplied by itself, in the other case subtracting the same half, and you will have a binomial and apotome respecitvely; then subtract the cube root of the apotome from the cube root of the binomial, and the remainder from this is the value of the unknown.

formal mathematics Bertrand’s postulate: HOL Light:

!n. ~(n = 0) ==> ?p. prime p /\ n <= p /\ p <= 2 * n

∀n. n ≠ 0 ⇒ ∃p. prime p ∧ n ≤ p ∧ p ≤ 2 · n

Mizar:

for n being Element of NAT st n>=1 holds
  ex p being Prime st n<p & p<=2*n

For all n being an element of the natural numbers such that n ≥ 1 holds that there exists a p being prime such that n < p and p ≤ 2n. submarines aren’t fishes

The question of whether machines can think is about as relevant as the question of whether submarines can swim.