词条 | Bar recursion |
释义 |
Bar recursion is a generalized form of recursion developed by C. Spector in his 1962 paper.[1] It is related to bar induction in the same fashion that primitive recursion is related to ordinary induction, or transfinite recursion is related to transfinite induction. Technical definitionLet V, R, and O be types, and i be any natural number, representing a sequence of parameters taken from V. Then the function sequence f of functions fn from Vi+n → R to O is defined by bar recursion from the functions Ln : R → O and B with Bn : ((Vi+n → R) x (Vn → R)) → O if:
Here "cat" is the concatenation function, sending p, x to the sequence which starts with p, and has x as its last term. (This definition is based on the one by Escardó and Oliva.[2]) Provided that for every sufficiently long function (λα)r of type Vi → R, there is some n with Ln(r) = Bn((λα)r, (λx:V)Ln+1(r)), the bar induction rule ensures that f is well-defined. The idea is that one extends the sequence arbitrarily, using the recursion term B to determine the effect, until a sufficiently long node of the tree of sequences over V is reached; then the base term L determines the final value of f. The well-definedness condition corresponds to the requirement that every infinite path must eventually pass through a sufficiently long node: the same requirement that is needed to invoke a bar induction. The principles of bar induction and bar recursion are the intuitionistic equivalents of the axiom of dependent choices.[3] References1. ^{{cite book|author=C. Spector|chapter=Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics|editor=F. D. E. Dekker|title=Recursive Function Theory: Proc. Symposia in Pure Mathematics|volume=5|pages=1–27|year=1962|publisher=American Mathematical Society}} {{DEFAULTSORT:Bar Recursion}}{{mathematics-stub}}2. ^{{cite journal|author=Martín Escardó|author2=Paulo Oliva|title=Selection functions, Bar recursion, and Backwards Induction|journal=Math. Struct. in Comp.Science|url=http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf}} 3. ^{{cite book|author=Jeremy Avigad|author-link=Jeremy Avigad|author2=Solomon Feferman|author2-link=Solomon Feferman|chapter=VI: Gödel's functional ("Dialectica") interpretation|title=Handbook of Proof Theory|editor=S. R. Buss|editor-link=S. R. Buss|year=1999|url=http://math.stanford.edu/~feferman/papers/dialectica.pdf}} 1 : Recursion |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。