I just saw this blog entry: Money vs. Decimal in SQL Server.

Which basically says that money has a precision issue...

declare @m money
declare @d decimal(9,2)

set @m = 19.34
set @d = 19.34

select (@m/1000)*1000
select (@d/1000)*1000

For the money type, you will get 19.30 instead of 19.34. I am not sure if there is an application scenario that divides money into 1000 parts for calculation, but this example does expose some limitations.

при условии, что Вы уже практиковались в функциональном программировании или комбинаторной логике.

---

Конечно, есть и другие вспомогательные средства, где мы можем оставаться в сфере логики:

• доказательство проблемы в какой-нибудь более интуитивной дедуктивной системе (например, естественная дедукция )
• и затем с использованием метатеорем , которые предоставляют возможность «компилятора»: перевод «высокоуровневого» доказательства естественной дедукции в «машинный код» Система дедукции в стиле Гильберта. Я имею в виду, например, металогическую теорему под названием « теорема дедукции ».

---

Что касается средств доказательства теорем, насколько мне известно, возможности некоторых из них расширены, так что они могут использовать интерактивный человеческий помощь. Например, Coq .

---

---

Приложение

Давайте посмотрим на пример. ⊢ α ⊃ β ⊃ α

Axiom scheme — chain rule:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [CR_α,β,γ]
⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ

Rule of inference — modus ponens:

⊢ α ⊃ β ⊢ α
━━━━━━━━━━━━━━━━━━━ [MP]
⊢ β

Proof tree

Let us see a tree diagram representation of the proof:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [CR_{α, α⊃α, α}] ━━━━━━━━━━━━━━━ [VEQ_{α, α⊃α}]
⊢ [ α ⊃ ( α ⊃ α ) ⊃ α ] ⊃ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α ⊢ α ⊃ ( α ⊃ α ) ⊃ α
━━━━━━━━━━━━━━━━ ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [ МП ] ━ ━━━━━━━━━━ [ VEQ _{α , α} ]
⊢ ( α ⊃ α ⊃ α ) ⊃ α ⊃ α ⊢ α ⊃ α ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━ [ МП ]
⊢ α ⊃ α

Proof formulae

Let us see an even conciser (algebraic? calculus?) representation of the proof:

(CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}) VEQ_α,α: ⊢ α⊃ α

so, we can represent the proof tree by a single formula:

• the forking of the tree (modus ponens) is rendered by simple concatenation (parentheses),
• and the leaves of the tree are rendered by the abbreviations of the corresponding axiom names.

It is worth of keep record about the concrete instantiation, that' is typeset here with subindexical parameters.

As it will be seen from the series of examples below, we can develop a proof calculus, where axioms are notated as sort of base combinators, and modus ponens is notated as a mere application of its "premise" subproofs:

Example 1

VEQ_α,β: ⊢ α ⊃ β ⊃ α

meant as

Verum ex quolibet axiom scheme instantiated with α,β provides a proof for the statement, that α ⊃ β ⊃ α is deducible.

Example 2

VEQ_α,α: ⊢ α ⊃ α ⊃ α

Verum ex quolibet axiom scheme instantiated with α,α provides a proof for the statement, that α ⊃ α ⊃ α is deducible.

Example 3

VEQ_{α, α⊃α}: ⊢ α ⊃ (α ⊃ α) ⊃ α

meant as

Verum ex quolibet axiom scheme instantiated with α, α⊃α provides a proof for the statement, that α ⊃ (α ⊃ α) ⊃ α is deducible.

Example 4

CR_α,β,γ: ⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ

meant as

Chain rule axiom scheme instantiated with α,β,γ provides a proof for the statement, that (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ is deducible.

Example 5

CR_{α,α⊃α,α}: ⊢ [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α

meant as

Chain rule axiom scheme instantiated with α,α⊃α,α provides a proof for the statement, that [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α is deducible.

Example 6

CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}: ⊢ (α ⊃ α⊃α) ⊃ α⊃ α

meant as

If we combine CR_{α,α⊃α,α} and VEQ_{α,α ⊃ α} together via modus ponens, then we get a proof that proves the following statement: (α ⊃ α⊃α) ⊃ α⊃ α is deducible.

Example 7

(CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}) VEQ_α,α: ⊢ α⊃ α

If we combine the compund proof (CR_{α,α⊃α,α}) together with VEQ_{α,α ⊃ α} (via modus ponens), then we get an even more compund proof. This proves the following statement: α⊃ α is deducible.

Combinatory logic

Although all this above has indeed provided a proof for the expected theorem, but it seems very unintuitive. It cannot be seen how people can "find out" the proof.

Let us see another field, where similar problems are investigated.

Untyped combinatory logic

Combinatory logic can be regarded also as an extremely minimalistic functional programming language. Despite of its minimalism, it entirely Turing complete, but evenmore, one can write quite intuitive and complex programs even in this seemingly obfuscated language, in a modular and reusable way, with some practice gained from "normal" functional programming and some algebraic insights, .

Adding typing rules

Combinatory logic also has typed variants. Syntax is augmented with types, and evenmore, in addition to reduction rules, also typing rules are added.

For base combinators:

• K_α,β is selected as a basic combinator, inhabiting type α → β → α
• S_α,β,γ is selected as a basic combinator, inhabiting type (α → β → γ) → (α → β) → α → γ.

Typing rule of application:

• If X inhabits type α → β and Y inhabits type α, then X Y inhabits type β.

Notations and abbreviations

• K_α,β: α → β → α
• S_α,β,γ: (α → β → γ) → (α → β)* → α → γ.
• If X: α → β and Y: α, then X Y: β.

Curry-Howard correspondence

It can be seen that the "patterns" are isomorphic in the proof calculus and in this typed combinatory logic.

• The Verum ex quolibet axiom of the proof calculus corresponds to the K base combinator of combinatory logic
• The Chain rule axiom of the proof calculus corresponds to the S base combinator of combinatory logic
• The Modus ponens rule of inference in the proof calculus corresponds to the operation "application" in combinatory logic.
• The "conditional" connective ⊃ of logic corresponds to type constructor → of type theory (and typed combinatory logic)

Functional programming

But what is the gain? Why should we translate problems to combinatory logic? I, personally, find it sometimes useful, because functional programming is a thing which has a large literature and is applied in practical problems. People can get used to it, when forced to use it in erveryday programming tasks ans pracice. And some tricks and hints of functional programming practice can be exploited very well in combinatory logic reductions. And if a "transferred" practice develops in combinatory logic, then it can be harnessed also in finding proofs in Hilbert system.

External links

Links how types in functional programming (lambda calculus, combinatory logic) can be translated into logical proofs and theorems:

• Wadler, Philip (1989). Theorems for free!.

Links (or books) how to learn methods and practice to program directly in combinatory logic:

• Madore, David (2003). The Unlambda Programming Language. Unlambda: Your Functional Programming Language Nightmares Come True.
• Curry, Haskell B. & Feys, Robert & Craig, William (1958). Combinatory Logic. Vol. I. Amsterdam: North-Holland Publishing Company.
• Tromp, John (1999). Binary Lambda Calculus and Combinatory Logic. Downloadable in PDF and Postscript from the author's John's Lambda Calculus and Combinatory Logic Playground.