Utilities and examples

  • Utilities for vectors
  • Syntax for the rowing machines
  • Modular syntax of types and terms
  • Polarized syntax with polyadic binders
  • General facts of Counter Machines as defined by Pierce
  • General facts of Counter Machines as defined in the Undecidability library
  • General facts of Rowing Machines
  • Unscoped syntax example
  • Well-scoped syntax example
  • Polyadic syntax example
  • Encoding of well-scoped syntax as unscoped syntax
  • Encoding of polyadic syntax as well-scoped syntax
  • Definitions

  • Counter machine definition and halting problem
  • Rowing machine definition and halting problem
  • System Fsub subtyping and typechecking problem
  • System Fsub subtyping without arrow types
  • (Normal) System Fsub definition and subtyping problem
  • (Deterministic) System Fsub definition and subtyping problem
  • (Flattened) System Fsub definition and subtyping problem
  • Reductions

  • Reduction from Counter Machines to Rowing Machines
  • Reduction from Counter Machines as defined in the Undecidability library to Counter Machines as defined by Pierce
  • Reduction from Rowing Machines to Flattened System Fsub
  • Reduction from Flattened System Fsub to Deterministic System Fsub
  • Reduction from the Deterministic System Fsub to the Normal System Fsub
  • Reduction from the Normal System Fsub to the full System Fsub
  • Reduction from typechecking in the Normal System Fsub with arrows to typechecking in the full System Fsub with arrows
  • Undecidability results

  • Undecidability of the halting problem of 2 Counter Machines a la Pierce
  • Undecidability of the halting problem of Rowing Machines
  • Undecidability of the subtyping problem of System FsubF
  • Undecidability of the subtyping problem of System FsubD
  • Undecidability of the subtyping and typechecking problems of System FsubN
  • Undecidability of the subtyping problem of System Fsub without arrow types
  • Undecidability of the subtyping and typechecking problems of System Fsub