# Today I Learned

Some of the things I've learned every day since Oct 10, 2016

## Category Archives: logic

## 69: The Deduction Theorem

December 20, 2016

Posted by on In logic, the **deduction theorem** states that where are formulas and is a set of assumptions or axioms, the implication is deducible from if and only if is deducible from . The statement is intuitive, but wasn’t formally proven until 1930.

## 51: Undecidability of Equality of Lambda Expressions

November 30, 2016

Posted by on In general, there is no algorithm which determines whether two lambda expressions are equivalent under the reduction rules of the lambda calculus. This is the problem for which the first proof of undecidability was given.

## 50: Normalization Property (Lambda Calculus)

November 29, 2016

Posted by on In a rewrite system, such as -reduction in the lambda calculus, a term may or may not satisfy either the weak normalization or the strong normalization property.

A term satisfies the **weak normalization property** if there exists a sequence of rewrites on that eventually results in a *normal form* of : a term which is irreducible.

A term satisfies the **strong**** normalization property** if *every* sequence of rewrites on eventually results in a normal form of .

If every term in a rewrite system satisfies the [weak | strong] normalization property, then the system itself is said to satisfy the same property.

Examples:

An example of a system which satisfies neither of the normalization properties is the pure untyped lambda calculus. An example of a non-normal term within this system is

.

Under -reduction, this term reduces to itself, and so it never terminates in an irreducible form.

Conversely, a term within this system which *is* weakly normal is

.

Under -reduction, this term reduces to just the variable , an irreducible term.

There are other forms of the lambda calculus, as well as other similar systems, which are normal. These can be viewed as programming languages in which every program eventually will (or can) terminate. A significant drawback to such a system, however, is that if a system is normal *it cannot be Turing complete*.

Additionally, in the lambda calculus every normalizing term has a *unique *normal form.

## 49: Church Numerals

November 28, 2016

Posted by on In Church encoding, an encoding system using lambda calculus, the **Church numerals** are the representation of the natural numbers. The distinguishing feature of the Church numerals is that the natural numbers are not treated as a primitive type, as they would typically be, but are simply represented by higher-order functions. Each higher-order function representing the number takes two arguments — a function and a second argument to be passed to — and returns the -fold composition of .

Examples:

0 is represented as , which given any function returns a function which simply returns without applying at all.

1 is represented as , which given any function returns a function which applies once to .

2 is represented as , which given any function returns a function which applies twice to .

3 is represented as , which given any function returns a function which applies three times to .

## Recent Comments