Inductively Defined Subsets

A statement like the following: "the set F⊆N of natural numbers is the least set of natural numbers satisfying

1. 0∈F, and
2. n∈F⇒f(n)∈F"

means that

• F satisfies (1) and (2), and
• if X⊆N also satisfies (1) and (2) then F⊆X.

In this case we say that F is inductively defined by the rules (1) and (2).

An alternative way of writing a rule is

	hypothesis
	----------
	conclusion
      

The rules (1) and (2) above could then be rewritten as:

	----
	0∈F

	  n∈F
	-------
	f(n)∈F
      

The form for a rule which defines a subset S of a set X is

	   x1∈S, ..., xn∈S
	R:-----------------
	        x∈S
      

The hypothesis is specified by the finite subset {x1, ..., xn}∈X. The conclusion is specified by an element x∈X. The subset S⊆X is closed under the rule R if x∈S whenever, x1∈S, ..., xn∈S.

A subset S of a set X is inductively defined by a collection of rules R if

1. S is closed under each rule in R
2. if S'⊆X is also closed under each rule in R, then S⊆S'.

Inductively defined subsets are unique. To see why, consider two subsets S1 and S2 which satisfy (1) and (2) above. In this case S1⊆S2 and S2⊆S1, so S1=S2.

We could also define S above as the intersection of all S'⊆X that are closed under each rule in R. Obviously S would also be a subset of R which is closed under each rule in R.

Simultaneously Inductively Defined Subsets

Given sets X1, ..., Xk, the subsets S1⊆X1, ..., Sk⊆Xk are inductively defined by a set of rules of the form

	   x1∈Si1, ..., xn∈Sin
	R:---------------------
	          x∈Si
      

where i, i1, ..., in∈{1, ...,k}, x∈Xi and x1∈Xi1, ...,xn∈Xin, provided

1. S1, ...,Sk are closed under each of the rules, and
2. if S'1, ...,S'k are also subsets of X1, ..., Xk and are closed under the rules, then S1⊆S'1, ...,Sk⊆Sk.

Example

As an example of an inductively defined subset, we'll construct the set of λ-terms of the λ-calculus.

The alphabet of λ-terms, Α, is defined as follows:

• variables: v0, v1, v2, ...,
• abstractor: λ,
• parentheses and dot: (, ), ..

We can define the set of λ-terms, Λ⊆Α*, as follows

	           
	Variable: ------
                   vi∈Λ

	Abstraction:   M∈Λ
		    ---------
		     λvi.M∈Λ

	Application: M∈Λ, N∈Λ
		     ---------
		      (M N)∈Λ

      

Proofs

Suppose we have subsets S1⊆X1, ...,Sk⊆Xk which are inductively defined by a set of rules R. A proof that x∈Si is a finite non-empty list:

	x1∈Si1, ..., xn∈Sin
      

such that

• x∈Si is the last entry in the list, i.e., the conclusion of the proof, and
• each element of the list xj∈Sij is the conclusion of a rule in R all of whose hypotheses occur in the list before xj∈Sij.

Proofs can be drawn as trees or written as lists. As an example here is a proof in list form of the claim that λv1λ.v2.v1∈Λ:

1. v1∈Λ [Variable rule]
2. λv2.v1∈Λ [Abstraction rule on (1)]
3. λv1λ.v2.v1∈Λ [Abstraction rule on (2)]

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.