TH0: The Monomorphic Higher-order Form

Overview

• Extends FOF with higher-order notions
• Curried form for type declarations
• Lambda terms (with a lambda binder) and symbol application
• Two other new binders

Types and Type Signatures

• Types
  • The predefined types $i and $o
  • The arithmetic types $int for integers, $rat for rationals, $real for reals
  • User-defined types (constants)
  • (τ₁ > ... > τ_n > τ^~) for n > 0
• About types
  • The (τ₁ > ... > τ_n > τ^~) type allows variables to have function types
  • The curried form allows for partial application

• Type Signatures
  • Individual types τ

New Binders and Connectives

• ^ is the lambda binder
• @ is (explicit) application
• @+ for the ι binder (indefinite description, aka choice)
• @- for the ε binder (definite description)

Notes

• Connectives can be used as terms
• Application can be partial
• Use of functions and predicates must respect the type signature

TH0 Example