Prev Up Next
Go backward to 1 What can be declared in a basic item?
Go up to Top
Go forward to 3 What is a function space?

2 Reduction to first-order logic

If possible, the semantics should be given via a reduction to first-order logic (see, e.g. [Hax97][Me93]). This has the advantage that we can re-use the theory developed for first-order logic. Since we are dealing with subsorted partial logic, we reduce subsorted partial higher-order to subsorted partial first-order logic3 by using a partial application operator for application of partial functions, and an application predicate for application of predicates.

For the current proposal, a reduction to first-order logic is possible, but for extensions like polymorphism, this yet has to be checked.

CoFI Note: L-8 ---- 7 January 1998.
Comments to

Prev Up Next