Some inductive definitions of sets

Documentation and user's manual

Table of contents

OCaml programs

Some inductive definitions of sets

The set N of all the natural numbers can be defined as follows Basis: zero() is in N. Induction: if x is in N then suc(x) is in N. Here B={zero} and I={suc}.

The set N of all the natural numbers can also be defined as follows Basis: zero() and one() are in N. Induction: if x is in N then sucsuc(x) is in N. Here B={zero,one} and I={suc}.

The set N of all the natural numbers can be defined as follows, too Basis: zero() is in N. Induction: If x is in N- {zero()} then d0(x) is in N. If x is in N then d1(x) is in N. Here B={zero} and I={d0,d1}.

The set of all the lists of integers, here denoted by L, can be defined as follows Basis: emptyList() is in L. Induction: if x is in L and i is in Z then consList(i)(x) is in L. Here B={emptyList} and I={consList(i), i in Z}.

The set Z[X] of all the polynomials in one variable X and whose coefficients are rational numbers can be defined as follows Basis: nullPoly() is in Z[X]. Induction: if p is in Z[X] and i is in Z then consPoly(i)(p) is in Z[X]. Here B={nullPoly} and I={consPoly(i), i in Z}. Note that if consPoly(i)(p) is interpreted as the polynomial i + Xp then this inductive definition of Z[X] is well-suited for easily defining (using the Horner scheme) the function that evaluates a polynomial.

The set of all the binary trees of integers, here denoted by T, can be defined as follows Basis: emptyTree() is in T. Induction: if (x1,x2) is a pair of elements of T and i is in Z then plant(i)(x1,x2) is in T. Here B={emptyTree} and I={plant(i), i in Z}.

The set of all the strings over an alphabet A, here denoted by Str, can be defined as follows Basis: emptyString() is in Str and if a in A then LengthOneString(a) is in Str. Induction: if x is in Str and (a1,a2) is a pair of elements of A then AddTwo(a1,a2)(x) is in Str. Here B={emptyString} union{LengthOneString(a), a in A} and I={AddTwo(a1,a2), (a1,a2) in A x A}. Note that if AddTwo(a1,a2)(x) is interpreted as the string whose characters are a1 followed by those of x in order followed by a2 then this inductive definition of strings is well-suited for easily defining the predicate function that checks whether reading a string from left to right is as reading it from right to left.

Some inductive definitions of sets

Documentation and user's manual

Table of contents

OCaml programs