Собственно, взял перерыв в своих собственных студенческих занятиях и читаю outline доказательства этого чувака. Красиво пишет, зараза. >Bellantoni, Cook, and Leivant have revealed a profound difference between polyno- mial-time recursions and all other recursions. The recursions constructed by the BCL schema enjoy a different ontological status from recursions in general. In the former, recursions are performed only on objects that have already been constructed. In the latter, for example in a superexponential recursion, one counts chickens before they are hatched (and the chicks that they produce as well).