Logic and Predicates
The type is defined as:, where is a type variable. This produces the following two definitions for the boolean values and :
(Note that the above two functions require three — not two — parameters. The latter two should be lambda expressions, but the first one should be a type. This fact is reflected in the fact that the type of these expressions is ; the universal quantifier binding the α corresponds to the Λ binding the alpha in the lambda expression itself. Also, note that is a convenient shorthand for, but it is not a symbol of System F itself, but rather a "meta-symbol". Likewise, and are also "meta-symbols", convenient shorthands, of System F "assemblies" (in the Bourbaki sense); otherwise, if such functions could be named (within System F), then there would be no need for the lambda-expressive apparatus capable of defining functions anonymously.)
Then, with these two -terms, we can define some logic operators (which are of type ):
There is no need for an IFTHENELSE function as one can just use raw -typed terms as decision functions. However, if one is requested:
will do. A predicate is a function which returns a -typed value. The most fundamental predicate is ISZERO which returns if and only if its argument is the Church numeral 0:
Read more about this topic: System F
Famous quotes containing the words logic and, logic and/or predicates:
“Logic and hope fade somewhat by thirty-six, when endings seem more like clear warnings than useful experience.”
—Jane O’Reilly, U.S. feminist and humorist. The Girl I Left Behind, ch. 2 (1980)
“...some sort of false logic has crept into our schools, for the people whom I have seen doing housework or cooking know nothing of botany or chemistry, and the people who know botany and chemistry do not cook or sweep. The conclusion seems to be, if one knows chemistry she must not cook or do housework.”
—Ellen Henrietta Swallow Richards (1842–1911)
“In the case of our main stock of well-worn predicates, I submit that the judgment of projectibility has derived from the habitual projection, rather than the habitual projection from the judgment of projectibility. The reason why only the right predicates happen so luckily to have become well entrenched is just that the well entrenched predicates have thereby become the right ones.”
—Nelson Goodman (b. 1906)