So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here.

There is a paper by S. Bellantoni et al. called "Higher Type Recursion, Ramication and Polynomial Time" which can be found here. It mentions a notation of a complete type denoted $!\sigma$ but I am having trouble understanding it. They have a reduction rule for it but I don't understand what the $\kappa$ is doing there or how these things are introduced. The best I can manage is that you can introduce a complete type anytime you want and you can get it's value out by applying some random value. This makes no sense however as this would make it a mere wrapper for incomplete types.

The reduction rule they give is

$(!r)\kappa \to r$

This reduction rule seems to suggest that the $!$ operator is like the K combinator.

They also give the semantics of $!r$ which seems to suggest that there is no difference

$[[!r]]_{!\sigma} = [[r]]_{\sigma}$ (I can't seem to figure out how to write semantic brackets properly)

Another clue as to what this thing means is the following reduction rule

$\mathcal{R} g h !(s_i n) \to h \kappa !(s_i n) !(\mathcal{R} g h !n)$

So it seems tell me that to make a term of complete type I can just use the $!$ operator on a term of incomplete type. It also tells us (where it gives the type of $\mathcal{R}$) that $h$ is of complete type so I can see that to get the corresponding incomplete type out of a complete type I can just apply some random term denoted by $\kappa$.

My interpretation must be wrong however because this would mean that there is no distinguishing difference between complete and incomplete terms.

My best guess is that there is a rule about the number of times incomplete types can be used in an expression that has not been specified as far as I can see. They even give something like this as the intuition of what a complete type is but I see no formal rules on the matter. Did I just miss it?

What does a complete type mean? How does it differ from an incomplete type?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.