2
$\begingroup$

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?

$\endgroup$

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.