The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The TPTP language is one of the keys to the success of the TPTP world. Originally the TPTP world supported only rst-order clause normal form (CNF). Over the years support for full rst-order form (FOF), monomorphic typed rstorder form (TF0), rank-1 polymorphic typed rst-order form (TF1), and monomorphic typed higher-order form (TH0) have been added. The TF0, TF1, and TH0 languages also include constructs for arithmetic. This paper introduces the TH1 form, an extension of TH0 with TF1-style rank-1 polymorphism. TH1 is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. The hope is that TH1 will be implemented in many popular ATP systems for typed higher-order logic.
It opens the door to useful middleware, such as monomorphizers and other translation tools that encode polymorphism in FOF or TH0. Many existing ATP and ITP systems for higher-order logic already implement some kind of polymorphism. TH1 has been designed in interaction with those systems' developers, and can provide an interoperability layer for their systems. The hope is that TH1 will be implemented in many popular ATP systems for typed higher-order logic.
Figure 1 shows the relationships between the various TPTP language forms, leading to TH1. TH1 combines two existing orthogonal extensions to the basic FOF language: the polymorphic TF1 and the higher-order TH0.1 Therefore, this paper rst presents the preceding TF0, TF1, and TH0 forms, whose features are then inherited in the TH1 form.
The remainder of this paper is organized as follows: Section 2 introduces the generic TPTP language, with a brief review of the well-known rst-order form. Sections 2.1 and 2.2 describe the monomorphic and polymorphic typed rst-order forms, and Section 2.3 describes the monomorphic typed higher-order form. Sections 3 and 4 are the heart of the paper, describing the syntax and semantics of the polymorphic higher-order form respectively. Section 5 explains the LF-based type checking system for the typed languages. Section 6 concludes.
CNF
FOF TF0 TF1
TH0
TH1 The TPTP language is a human-readable, easily machine-parsable, exible and extensible language, suitable for writing both ATP problems and solutions. The top level building blocks of the TPTP language are annotated formulae. An annotated formula has the form:
language(name, role, formula, [source, [useful info]]).
The languages supported are clause normal form (cnf), rst-order form (fof), typed rst-order form (tff), and typed higher-order form (thf). The role, e.g., axiom, lemma, conjecture, de nes the use of the formula in an ATP system. In the formula, terms and atoms follow Prolog conventions, i.e., functions and predicates start with a lowercase letter or are 'single quoted', variables start with an uppercase letter, and all contain only alphanumeric characters and underscore. The TPTP language also supports interpreted symbols, which either start with a $, or are composed of non-alphanumeric characters, e.g., the truth constants $true and $false, and integer/rational/real numbers such as 27, 43/92, -99.66. The basic logical connectives are !, ?, ~, |, &, =>, <=, <=>, and <~>, for 8, 9, :, _, ^, ), (, ,, and respectively. Equality and inequality are expressed as the in x operators = and !=. An example annotated rst-order formula, supplied from a le, is: fof(union,axiom, ( ! [X,A,B] :
( member(X,union(A,B)) <=> ( member(X,A)
| member(X,B) ) ) file('SET006+0.ax',union), [description('Definition of union'), relevance(0.9)]). 1Note that while TH1 adopts features of TF1, TH0 is independent of TF0. 2.1
The Monomorphic Typed First-order Form TF0 TF0 extends the basic FOF language with types and type declarations. Every function and predicate symbol is declared before its use, with a type signature that speci es the types of the symbol's arguments and result.
have the following forms: the prede ned types $i for (individuals) and $o for o (booleans); the prede ned arithmetic types $int (integers), $rat (rationals), and $real (reals); user-de ned types (constants).
User-de ned types are declared (before their use) to be of the kind $tType, in annotated formulae with a type role { see Figure 2 for examples. All symbols share the same namespace; in particular, a type cannot have the same name as a function or predicate symbol.
TF0 type signatures & have the following forms: ( 1 * * n) > ~ for n > 0, where i are the argument types, and ~ is the result type. Argument types and the result type for a function cannot be $o, and the result type for a predicate must be $o. If n = 1 the parentheses are omitted.
The type signatures of uninterpreted symbols are declared like types, in annotated formulae with a type role {
see Figure 2 for examples. The type of = is ad hoc polymorphic over all types except $o, with both arguments
having the same type and the result type being $o. The types of arithmetic predicates and functions are ad hoc
polymorphic over the arithmetic types; see [
In logical formulae the arguments to functions and predicates must respect the symbol's type signature. Variables must be typed in their quanti cation, and used accordingly. For example, in Figure 2 the predicate chased is declared to have the type signature
(dog * cat) > $o so an example of a well-formed formula is
! [X: dog] : chased(X,garfield) because X is of type dog and garfield is of type cat.
Figure 2 illustrates some TF0 formulae, whose conjecture can be proved from the axioms (it is the TPTP problem PUZ130 1.p). 2.2
The Polymorphic Typed First-order Form TF1 TF1 extends TF0 with (user-de ned) type constructors, type variables, polymorphic symbols, and one new binder.
TF1 types
have the following forms: the prede ned types $i and $o; the prede ned arithmetic types $int, $rat, and $real; user-de ned n-ary type constructors applied to n type arguments; type variables, which must be quanti ed by !> { see the type signature forms below.
Type constructors are declared (before their use) to be of the kind ($tType * * $tType) > $tType, in annotated formulae with a type role. The type constructor's arity is the number of \$tType"s before the >. If the arity is zero the > is omitted, and the type constructor is a monomorphic user-de ned type constant as in TF0, else it is polymorphic. If the arity is less than two the parentheses are omitted. In the example of Figure 3, cup of is a unary type constructor that is is used to construct the type cup of(beverage)).
TF1 type signatures & have the following forms: %-----------------------------------------------------------------------------tff(animal_type,type,( animal: $tType )). tff(cat_type,type,( cat: $tType )). tff(dog_type,type,( dog: $tType )). tff(human_type,type,( human: $tType )). tff(cat_to_animal_type,type,( cat_to_animal: cat > animal )). tff(dog_to_animal_type,type,( dog_to_animal: dog > animal )). tff(garfield_type,type,( garfield: cat )). tff(odie_type,type,( odie: dog )). tff(jon_type,type,( jon: human )). tff(owner_of_type,type,( owner_of: animal > human )). tff(chased_type,type,( chased: ( dog * cat ) > $o )). tff(hates_type,type,( hates: ( human * human ) > $o )). tff(human_owner,axiom,( ! [A: animal] : ? [H: human] : H = owner_of(A) )). tff(jon_owns_garfield,axiom,(
jon = owner_of(cat_to_animal(garfield)) )). tff(jon_owns_odie,axiom,(
jon = owner_of(dog_to_animal(odie)) )). tff(jon_owns_only,axiom,( ! [A: animal] : ( jon = owner_of(A) => ( A = cat_to_animal(garfield) | A = dog_to_animal(odie) ) ) )). tff(dog_chase_cat,axiom,( ! [C: cat,D: dog] : ( chased(D,C) => hates(owner_of(cat_to_animal(C)),owner_of(dog_to_animal(D))) ) )). tff(odie_chased_garfield,axiom,(
chased(odie,garfield) )). tff(jon_hates_jon,conjecture,(
hates(jon,jon) )). %-----------------------------------------------------------------------------( 1 * * n) > ~ for n > 0, where i are the argument types and ~ is the result type (with the same caveats as for TF0); !>[ 1: $tType, : : : , n: $tType]: & for n > 0, where 1; : : : ; n are distinct type variables and & is a type signature.
The binder !> in the last form denotes universal quanti cation in the style of calculi. It is only used at the top level in polymorphic type signatures. All type variables must be of type $tType; more complex type variables, e.g., $tType > $tType are beyond rank-1 polymorphism. In the example of Figure 3, the type signature for mixture is polymorphic. As in TF0, arithmetic symbols and equality are ad hoc polymorphic.
Type variables that are bound by !> without occurring in a type signature's body, e.g., as in the last example, are called phantom type variables. These make it possible to specify operations and relations directly on types and provide a convenient way to encode type classes. For example, a polymorphic propositional constant is linear can be declared with the type signature !>[A : $tType]: $o, and used as a guard to restrict the axioms specifying that a binary predicate less eq with the type signature !>[A: $tType]: ((A * A) > $o) is a linear order to those types that satisfy the is linear predicate, i.e., a formula of the form ! [A: $tType] : ( (is linear @ A) => (axiom about less eq)).
In logical formulae the application of symbols must respect the symbol's type signature. Additionally, every use of a polymorphic symbol (except ad hoc polymorphic arithmetic and equality symbols) must explicitly specify the type instance. A function or predicate symbol with a type signature !>[ 1: $tType, : : : , m: $tType]: (( 1 * > n > ~) must be applied to m type arguments and n term arguments. For example, in Figure 3 below, the type contructor cup of, the function full cup, the function mixture, and the predicate help stay awake, are declared to have the type signatures $tType > $tType beverage > cup of(beverage) !>[BeverageOrSyrup: $tType] : ((BeverageOrSyrup * syrup) > BeverageOrSyrup) cup of(beverage) > $o so an example of a well-formed formula is
! [S: syrup] : help stay awake(full cup(mixture(beverage,coffee,S))) because beverage provides the one type argument for mixture, coffee is of that type, S is of type syrup, and the result type is beverage as required by full cup, whose whose result type is in turn cup of(beverage) as required by help stay awake. As TF1 is rank-1 polymorphic, the type arguments must be actual types; in particular $tType and !>-binders cannot occur in type arguments of polymorphic symbols.
Figure 3 illustrates some TF1 formulae, whose conjecture can be proved from the axioms (it is a variant of the TPTP problem PUZ139 1.p). 2.3
The Monomorphic Typed Higher-order Form TH0 TH0 extends FOF with higher-order notions, including adoption of curried form for type declarations, lambda terms (with a lambda binder), symbol application, and two other new binders.
have the following forms: the prede ned types $i and $o; the prede ned arithmetic types $int, $rat, and $real; user-de ned types (constants); TH0 type signatures & have the following forms: individual types . ( 1 > > n > ~) for n > 0, where i are the argument types and ~ is the result type. %-----------------------------------------------------------------------------ff(beverage_type,type,( beverage: $tType )). tff(syrup_type,type,( syrup: $tType )). tff(cup_of_type,type,( cup_of: $tType > $tType )). tff(full_cup_type,type,( full_cup: beverage > cup_of(beverage) )). tff(coffee_type,type,( coffee: beverage )). tff(vanilla_type,type,( vanilla: syrup )). tff(caramel_type,type,( caramel: syrup )). tff(help_stay_awake_type,type,( help_stay_awake: cup_of(beverage) > $o )). tff(mixture_type,type,( mixture: !>[BeverageOrSyrup: $tType] :
( ( BeverageOrSyrup * syrup ) > BeverageOrSyrup ) )). %----Coffee keeps you awake tff(mixture_of_coffee_help_stay_awake,axiom,(
! [S: syrup] : help_stay_awake(full_cup(mixture(beverage,coffee,S))) )). %----Coffee mixed with a syrup or two helps you stay awake tff(syrup_coffee_help_stay_awake,conjecture,( help_stay_awake(full_cup(
mixture(beverage,coffee,mixture(syrup,caramel,vanilla)))) )). %-----------------------------------------------------------------------------The ( 1 > > n > ~) form is promoted to be a type in TH0 (and TH1) forms, so that variables in formulae can be quanti ed as function types. The curried form means that TH0 provides the possibility of partial application. As in TF0, arithmetic symbols and equality are ad hoc polymorphic.
The new binary connective @ represents application (explicit use of @ is required { symbols cannot simply be juxtaposed) { see Figure 4 for examples. There are three new binders: ^, @+, and @-, for , (inde nite description, aka choice), and (de nite description). Use of all the connectives as terms is also supported { this is quite straightforward because connectives are equivalent (in Henkin semantics - see below) to corresponding lambda abstractions. The arithmetic predicates and functions, and the equality operator, can also be used as terms, but must be applied to a term of a known type (which must be an arithmetic type for the arithmetic symbols). This formula illustrates the use of conjunction as a term, in a de nition of f alse, thf(and_false,definition,( ( ( & @ $false ) = ( ^ [Q: $o] : $false ) ) )).
In logical formulae the application of symbols must respect the symbol's type signature. For example, in Figure 4 the symbols mix and hot are declared to have the type signatures beverage > syrup > beverage beverage > $o so an example of a well-formed formula is
! [S: syrup] : (hot @ (mix @ coffee @ S)) because S is of type syrup, coffee is of type beverage, and mix the result type is beverage as required by hot. Partial application results in a lambda term. For example, mix @ coffee produces a lambda term of type syrup > beverage.
Figure 4 illustrates some TH0 formulae, whose conjecture can be proved from the axioms (it is a variant of the TPTP problem PUZ140^1.p). The following formula illustrates the de nite description binder (the inde nite and de nite description binders are not used in Figure 4) for a set whose elements of type $i are all equal,
The semantics for TH0 is Henkin semantics with choice (Henkin semantics by de nition also includes Boolean
and functional extensionality) [
( coffee_mixture = ( mix @ coffee ) )). %----Any coffee mixture is hot coffee thf(coffee_and_syrup_is_hot_coffee,axiom,( ! [S: syrup] : ( ( (coffee_mixture @ S) = coffee )
& ( hot @ ( coffee_mixture @ S ) )) )). %----There is some mixture of coffee and any syrup which is hot coffee thf(there_is_hot_coffee,conjecture,( ? [SyrupMixer: syrup > beverage] : ! [S: syrup] : ? [B: beverage] :
( ( B = ( SyrupMixer @ S ) ) & ( B = coffee ) & ( hot @ B ) ) )). %-----------------------------------------------------------------------------
TH1 combines the higher-order features of TH0 (curried form, lambda terms, description, partial application) with the polymorphic features of TF1 (type constructors, type variables, polymorphic symbols). TH1 also adds ve new polymorphic constants.
TH1 types
have the following forms: the prede ned types $i and $o; user-de ned n-ary type constructors applied to n type arguments; type variables (which must be quanti ed by !>); ( 1 >
> n > ~) for n > 0, where i are the argument types and ~ is the result type.
individual types; !>[ 1: $tType, : : : , n: $tType]: & for n > 0, where 1; : : : ; n are distinct type variables and & is a type signature.
In logical formulae the application of symbols must respect the symbol's type signature. Additionally, as in TF1, every use of a polymorphic symbol must explicitly specify the type instance by providing type arguments. However, in TH1 the application to terms may be partial, i.e., a symbol with a type signature !>[ 1: $tType, : : : , m: $tType]: ( 1 > > n > ~) must be applied to m type arguments and up to n term arguments. For example, given the type declarations in Figure 5 below, some examples of well-formed formulae are idempotent @ bird @ ^ [X: bird] : X ! [M: map @ bird @ $o] : ( bird lookup @ bird @ $o @ M @ tweety ) ! [T: $tType] : ( idempotent @ T @ ^ [X: T] : X ).
TH1 has ve new polymorphic constants: !! for (universal quanti cation), ?? for (existential quanti cation), @@+ for (inde nite description, aka choice), @@- for (de nite description), and @= (equality).2 Each of these must be instantiated by applying them to exactly one type argument, e.g.,
? [B: bird] : ( (@= @ bird) @ tweety @ B ).
Figure 5 illustrates some TH1 formulae, whose conjecture can be proved from the axioms. It declares and axiomatizes lookup and update operations on maps, then conjectures that update is idempotent for certain keys and values. Figure 6 illustrates the !! universal quanti cation operator by de ning apply both as the function that supplies its argument to the function as both its arguments, then conjecturing that the two are equal for all types. Figure 7 illustrates the @@- inde nite description operator by asserting that the function has fixed point has a xed point (some X such that f(X) = X), and then conjecturing that applying the function to some xed point simply returns that xed point. In informal mathematics, there is no guarantee that the two \some xed point" expressions are equal, e.g., if has fixed point is the identity function then all points are xed points. However, in logic, \some xed point" has a xed interpretation in a given model, so the conjecture is a theorem. Figure 8 illustrates the @= equality connective by de ning the higher-order is symmetric predicate that takes a predicate as an argument and returns true i the argument is a symmetric predicate, and then conjecturing that @= is symmetric (which it is). %-----------------------------------------------------------------------------thf(bird_type,type,( bird: $tType )). thf(tweety_type,type,( tweety: bird )). thf(list_type,type,( list: $tType > $tType )). thf(map_type,type,( map: $tType > $tType > $tType )). tff(bird_lookup_type,type,(
bird_lookup: !>[A: $tType,B: $tType] : ( ( map @ A @ B ) > A > B ) )). thf(bird_update_type,type,( bird_update: !>[A: $tType,B: $tType] :
( ( map @ A @ B ) > A > B > ( map @ A @ B ) ) )). thf(idempotent_type,type,( idempotent: ( !>[A: $tType] : ( A > A ) > $o ) )).
The semantics of TH1 have to extend that of TH0 and that of TF1, to maximize the uniformity of the TPTP. Additionally, the semantics have be compatible with that of existing higher-order logic proof assistants and 2!! and ?? used to be in TH0, but they have been moved out to be in only TH1 now. thf(apply_both_defn,axiom,(
apply_both = ( ^ [X: a_type] : ( the_function @ X @ X ) ) )). thf(prove_this,conjecture, ( !! @ a_type @ ^ [Y: a_type] : ( ( the_function @ Y @ Y ) = ( apply_both @ Y ) ) )). %-----------------------------------------------------------------------------%-----------------------------------------------------------------------------thf(a_type,type,( a_type: $tType )). thf(has_fixed_point_type,type,( has_fixed_point: a_type > a_type )). thf(apply_has_fixed_point,axiom,(
? [X: a_type] : ( ( has_fixed_point @ X ) = X ) )). %-----------------------------------------------------------------------------thf(a_type,type,(
a_type: $tType )). thf(is_symmetric_type,type,(
is_symmetric: ( ( $i > a_type ) > ( $i > a_type ) > $o ) > $o )). thf(conj,conjecture,
( is_symmetric @ ( @= @ ( $i > a_type ) ) )). %-----------------------------------------------------------------------------countermodel nders, so as to provide a problem exchange language for such tools.
The semantics of TH1 is, as for TH0, the Henkin semantics with choice, extended to shallow polymorphism
[
The rst three rules introduce the re exivity and transitivity of equality, and assumption: t : bool ` t = t 1 ` s = t
2 ` t = u 1 [ 2 ` s = u fpg ` p The next two de ne application and abstraction over equality theorems: 1 ` f = g 2 ` x = y f : ->
x :
1 ` s = t 1 ` (^[x: ]:s) = (^[x: ]:t)
The next three correspond to beta reduction, modus ponens for equalities, and deduction of logical equivalence from deductions in both directions:
t : -> ` (^[x: ]:t)(x: ) = t 1 ` s = t
2 ` s 1 [ 2 ` t 1
1 ` p fqg [ 2 2 ` q fpg ` p = q The nal two rules allow for instantiation of types and terms in proven theorems: [ 1; :::; n] ` p[ 1; :::; n] [ 1; :::; n] ` p[ 1; :::; n] [x1; :::; xn] ` p[x1; :::; xn] [t1; :::; tn] ` p[t1; :::; tn]
In order to achieve the exact semantics of the higher-order logic provers, it is necessary to add axioms that correspond to those of the provers. For example, HOL Light introduces three axioms: eta (from which classical logic follows), in nity (which allows the de nition an in nite type of individuals, out of which the natural numbers are carved), and choice. To achieve the Henkin semantics (including the induced classical logic) the eta axiom is added. The in nity axiom is not needed because TH1 problems introduce the necessary types as assumptions. Two instances of the axiom of choice are given: one for choice and one for description. They specify the operators @++ and @--. None of the axioms need any inference assumptions, so they can be given in the TPTP syntax. thf(eta,axiom,( ! [A: $tType,B: $tType,A0: ( A > B )] :
( ( ^ [A1: A] : ( A0 @ A1 ) ) = A0 ) )). thf(choice_type,type,(
@@+: !>[A: $tType] : ( ( A > $o ) > A ) )).
Well-typed TPTP formulae are de ned uniformly for CNF, FOF, TF0, TF1, TH0, and TH1 using a set of
typing rules. We use the logical framework LF [
The type-checking process is split into two steps. The rst step translates a TPTP problem P to a Twelf
theory P . This step is implemented as part of the TPTP2X tool, and is a relatively simple induction on the
context-free grammar for TPTP. The second step runs Twelf to check the theory T H1; P . This includes, in
particular, the context-sensitive parts of the language. This is the same process as used for TH0 [
Besides bridging the minor syntactic di erences between TPTP and Twelf, this step performs two basic structural checks:
It reject formulae not allowed in the respective language form, e.g., it rejects polymorphic type signatures in TF0 formula.
It translates all formulae into TH1.
The translation into TH1 proceeds as follows:
CNF to FOF: This well-known and straightforward translation has been part of the TPTP tool suite for some time.
FOF to TF0: This is essentially an inclusion. The only subtlety is that the untyped FOF constants and quanti ers must become typed. This is done by assuming that every untyped n-ary function or predicate symbol has type signature ($i * ... * $i) > $i or ($i * ... * $i) > $o, respectively. Moreover, all FOF variables are taken to range over the type $i.
TF0 to TF1, and TH0 to TH1: These translations are inclusions.
TF0 to TH0, and TF1 to TH1: These translations are almost inclusions. The only subtlety is that TF0/1 type signatures using * are translated to TH0/1 type signatures using >.
The inference system is a straightforward variant of the one used for TH0 [
(infix) These declare the LF type $tType of TPTP types, as well as $i, $o, and > as constructors for it. User-declared n-ary type operators T are translated to Twelf constants T: $tType -> ... -> $tType -> $tType.
The rules for terms are : $tType -> type : ($tm A -> $tm B) -> $tm (A > B) : $tm (A > B) -> $tm A -> $tm B
(infix) These declare the LF type $tm A of TPTP terms of type A for every TPTP type A:$tType, as well as constructors for ^ (using higher-order abstract syntax) and @. The latter two constructors take two implicit arguments A and B of type $tType, which are inferred by Twelf. User-declared (monomorphic) constants f of type are translated to Twelf constants f: $tm , where is the recursive translation of .
The rules for the remaining term constructors are as follows (omitting the constructors for propositional
formulae described in [
There is no need for rules for proofs, except for a truth predicate $istrue : $tm $o -> type This allows user-declared axioms and conjectures a asserting F to be represented as Twelf constants a:$istrue F.
Rank-1 polymorphism comes for free when using LF [
In addition to the ve term constructors, whose types are given above, TH1 also introduces ve corresponding constants. Besides being a part of TH1, they serve as examples of how polymorphic constants are represented in Twelf: !! : {A: $tType} $tm ((A > $o) > $o) ?? : {A: $tType} $tm ((A > $o) > $o) @@+: {A: $tType} $tm ((A > $o) > A ) @@-: {A: $tType} $tm ((A > $o) > A ) @= : {A: $tType} $tm ( A > A > $o) 6
This paper has described the polymorphic typed-higher order form (TH1) in the TPTP language family, which
extends the monomorphic TH0 language with TF1-style rank-1 polymorphism. A type-checker for the language
has been developed. Now that the language has been speci ed, TH1 problems can be added to the TPTP problem
library. Already hundreds of problems have been collected from various sources, e.g., the HOL(y)Hammer and
Sledgehammer exports from HOL [
A
The Twelf TH1 Theory $kind : type. %% types (i, o, functions and products) $tf : $kind -> type. $type : $kind. $tType = $tf $type. $i : $tType. $o : $tType. > : $tType -> $tType -> $tType. * : $tType -> $tType -> $tType. %% terms (lambda and application) $tm : $tType -> type. ^ : ($tm A -> $tm B) -> $tm (A > B). @ : $tm (A > B) -> $tm A -> $tm B. %% connectives $true : $tm $o. & : $tm $o -> $tm $o -> $tm $o. | : $tm $o -> $tm $o -> $tm $o. ~ : $tm $o -> $tm $o. $false : $tm $o
= ~ $true. => : $tm $o -> $tm $o -> $tm $o
= [a][b](a | ~ b). <= : $tm $o -> $tm $o -> $tm $o
= [a][b](b => a). <=> : $tm $o -> $tm $o -> $tm $o
= [a][b]((a => b) & (b => a)). <~> : $tm $o -> $tm $o -> $tm $o
= [a][b] ~ (a <=> b). ~& : $tm $o -> $tm $o -> $tm $o
= [a][b] ~ (a & b). ~| : $tm $o -> $tm $o -> $tm $o
= [a][b] ~ (a | b). %% equality over a type A == : $tm A -> $tm A -> $tm $o. != : $tm A -> $tm A -> $tm $o = [x][y] ~ (x == y). %infix right 10 >.
%infix right 10 *. %infix left 5 &. %infix left 5 |. %infix none 5 =>. %infix none 5 <=. %infix none 5 <=>. %infix none 5 <~>. %infix none 5 ~&. %infix none 5 ~|. %infix none 10 ==. %infix none 10 !=. %% quantification over a type A, taking a meta-level function ! : ($tm A -> $tm $o) -> $tm $o. %prefix 5 !. ? : ($tm A -> $tm $o) -> $tm $o
= [f] ~ (! [x] ~ (f x)). %prefix 5 ?. %% equality and quantifiers over types =t= : $tm A -> $tm A -> $tm $o. !t! : ($tType -> $tm $o) -> $tm $o. ?t? : ($tType -> $tm $o) -> $tm $o. %% dependent sum and product type %% ?* : ($tm A -> $tType) -> $tType. %% !> : ($tm A -> $tType) -> $tType. %% arithmetic types as a subtype $arithdom : type. $_int : $arithdom. $_rat : $arithdom. $_real : $arithdom. $arithtype : $arithdom -> $tType. $int : $tType = $arithtype $_int. $rat : $tType = $arithtype $_rat. $real : $tType = $arithtype $_real. %% dummy constants to represent arithmetic literals $intliteral : $tm $int. $ratliteral : $tm $rat. $realliteral : $tm $real. %% arithmetic operations in higher-order style for an arbitrary arithmetic type $less : $tm ($arithtype D) > ($arithtype D) > $o. $lesseq : $tm ($arithtype D) > ($arithtype D) > $o. $greater : $tm ($arithtype D) > ($arithtype D) > $o. $greatereq : $tm ($arithtype D) > ($arithtype D) > $o. $uminus : $tm ($arithtype D) > ($arithtype D). $sum : $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $difference: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $product : $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $quotient : $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $quotient_e: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $quotient_t: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $quotient_f: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $remainder_e: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $remainder_t: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $remainder_f: $tm ($arithtype D) > ($arithtype D) > ($arithtype D). $is_int : $tm ($arithtype D) > $o. $is_rat : $tm ($arithtype D) > $o. $is_real : $tm ($arithtype D) > $o. %% truth predicate $istrue : $tm $o -> type.