Types are propositions, functions are proofs

In a pure functional languages based on substitution, such as Simply Typed Lambda Calculus, various systems of various Logic, or high level languages like Miranda or Haskell, types could be viewed as propositions, while semantically correct pure functions (without side effects) define (or implement) actual proofs.

Each sub-expression inside a pure function (which as a whole is one single expression) has its own type.

Nested functions corresponds to a program, which is a single expression too. (The result of evaluation of main :: IO () in Haskell is an expression to be evaluated (reduced to a value) by the runtime.

The proof of an implication B → A is a function, which takes a proof of the antecedent B (a value from a nested function) into a proof of the consequent A. This.

The function that proves B → A is applied to the proof of B to yield a proof of A (which is a value).

Introduction + elimination (reduction) is a transition - a step further, preserving the Truth.

This is the formal logic.

The reduction rule for functions applies when a lambda term introduces a function, which is immediately eliminated by an application (apply).

Similarly, the reduction rules for Pairs apply when a constructor CONS introduces a Pair, which is immediately eliminated by a selector CAR or CDR.

There is nothing extra to it.

Start from the types, and the terms and reductions follow. The terms follow as introducers (define and eliminators apply for the type, and the reductions follow when an introducer meets an eliminator (inside eval which calls apply), and type safety follows by showing that each of the reduction rules preserves type derivations, which means the whole thing is consistent (without any contradiction).

This is what is called well-typed, type-sage or fp-complete - consistency guarantee.

Provided that semantics of each function (or proof) are correct, the whole program, then, is correct. The way some Math or Logic is correct.

Last modified 15 months ago Last modified on Nov 23, 2018, 7:59:27 AM
Note: See TracWiki for help on using the wiki.