Idempotent relation

In mathematics, an idempotent binary relation R  X × X is one for which R  R = R.[1][2] This notion generalizes that of an idempotent function to relations. Each idempotent relation is necessarily transitive, as the latter means R  R  R.

For example, the relation < on is idempotent. In contrast, < on is not, since (<)  (<)  (<) does not hold: e.g. 1 < 2, but 1 < x < 2 is false for every x  ℤ.

Idempotent relations have been used as an example to illustrate the application of Mechanized Formalisation of mathematics using the interactive theorem prover Isabelle/HOL. Besides checking the mathematical properties of finite idempotent relations, an algorithm for counting the number of idempotent relations has been derived in Isabelle/HOL. [3][4]

References

  1. Florian Kammüller, J. W. Sanders (2004). Idempotent Relation in Isabelle/HOL (PDF) (Technical report). TU Berlin. p. 27. 2004-04. Here:p.3
  2. Florian Kammüller (2011). "Mechanical Analysis of Finite Idempotent Relations". Fundamenta Informaticae. 107. pp. 43–65. doi:10.3233/FI-2011-392.
  3. Florian Kammüller (2006). "Number of idempotent relations on n labeled elements". The On-Line Ecyclopedea of Integer Sequences (A12137).
  4. Florian Kammüller (2008). Counting Idempotent Relations (PDF) (Technical report). TU Berlin. p. 27. 2008-15.


This article is issued from Wikipedia - version of the 6/10/2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.