Define a concept of bounds which extends to all quantifiable types. A product or coproduct has left and right bounds. A function type has domain and codomain bounds. A list or maybe type has a bound on the values. A map type has a bound on the keys and a bound on the values.
A bound on a scalar type is expressed as a term denoting a scalar of that type.
All quantifiers must be bounded.
This allows for the transformation to Sigma^1_1 formulas with bounded quantifiers to be semantics-preserving and straightforward.
morganthomas
commented
2 years ago
Define a concept of bounds which extends to all quantifiable types. A product or coproduct has left and right bounds. A function type has domain and codomain bounds. A list or maybe type has a bound on the values. A map type has a bound on the keys and a bound on the values.
A bound on a scalar type is expressed as a term denoting a scalar of that type.
All quantifiers must be bounded.
This allows for the transformation to Sigma^1_1 formulas with bounded quantifiers to be semantics-preserving and straightforward.