Polynomial-time list operations #
List operations for the polynomial-time calculus, using Christian Reitwiessner's encodings,
degree-bounded operations and fold rules. Indices use encUnary: an index returned by idxOf
is at most the list length, irrespective of the encoding of its elements. In particular, looking
up a variable with a large binary label does not require a certificate as long as that label.
Predicate counts and Boolean scans use only ListEncoding and SizedListEncoding: reading the
list and bounding traversal suffice because the state is a unary counter or a Boolean. Raw bit
strings and framed lists are both instances. No output-list construction capability is needed;
counting folds a counter directly instead of constructing the matching sublist.
Main results #
Turing.MultiTapeTM.ComputableTidilyInPolyTime.filter: filtering by a polytime predicate.Turing.MultiTapeTM.ComputableTidilyInPolyTime.cons,.listAppend,.map,.flatten: constructing lists.Turing.MultiTapeTM.ComputableTidilyInPolyTime.cons',.listAppend': composition rules that letfun_propinfer the element encoding from the result.Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapWith,.flatMapWith: constructing lists with a parameter; the input list may itself have polynomial encoded length.Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapWithInput,.flatMapWithInput,.filterWithInput,.findWithInput,.anyWithInput,.allWithInput: automation rules for traversals whose body also uses the original input.Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapConst,.flatMapConst,.allConst,.anyConst: traverse a fixed list without requiring an encoding of its elements.Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapFilterConst: select and map fixed parameters with computed guards and outputs, preserving list order and duplicates.Turing.MultiTapeTM.ComputableInPolyTime.mapConst,.flatMapConst,.mapFilterConst: plain certificates for fixed-list templates, without encoding the fixed parameters.Turing.MultiTapeTM.ComputableTidilyInPolyTime.filterWith,.findWith: filtering or searching a polynomial-time list with a parameterized test.Turing.MultiTapeTM.ComputableTidilyInPolyTime.length,.range,.replicate: unary lengths, ranges and lists of a computed length, charging each repeated value.Turing.MultiTapeTM.ComputableTidilyInPolyTime.zipIdx: number list entries with unary indices.Turing.MultiTapeTM.ComputableTidilyInPolyTime.zip: pair entries of framed lists.Turing.MultiTapeTM.ComputableTidilyInPolyTime.anyWith,.allWith: Boolean scans with a parameter, applied explicitly like the fold rules.Turing.MultiTapeTM.ComputableTidilyInPolyTime.countPWith,.anyWithEncoding,.allWithEncoding: direct scans over readable, size-bounded list encodings.Turing.MultiTapeTM.ComputableTidilyInPolyTime.countPWithInput,.countWithInput: count predicate matches or occurrences of a computed value.Turing.MultiTapeTM.ComputableTidilyInPolyTime.idxOf: the first occurrence of an element.Turing.MultiTapeTM.ComputableTidilyInPolyTime.listGetD: lookup by a unary index.Turing.MultiTapeTM.ComputableTidilyInPolyTime.listGetD_binary: lookup by a binary index, which is capped at the length of the list.Turing.MultiTapeTM.ComputableTidilyInPolyTime.getElem?: optional lookup in computed lists.Turing.MultiTapeTM.ComputableTidilyInPolyTime.listIsEmpty,.listIsEmpty',.bitsIsEmpty,.head?: inspect a list without a default element, with inference rules for framed and raw lists.Turing.MultiTapeTM.ComputableTidilyInPolyTime.listReverse,.listReverseWithInput: reverse framed lists, charging the complete encoded size of every intermediate prefix.Turing.MultiTapeTM.ComputableTidilyInPolyTime.idxOfWithInput,.bitsGetDWithInput: compositional rules for first-occurrence lookup and raw-bit access.Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsDropWithInput,.bitsTakeWithInput: runtime bit-string slicing, with computed unary indices.Turing.MultiTapeTM.ComputableTidilyInPolyTime.takeUnary,.listTakeWithInput,.listDropWithInput: slice framed lists at computed unary indices.Turing.MultiTapeTM.bits_encList_polyTime,.trans_encList_polyTime: convert between raw binary words and framed lists of encoded bits, also after an arbitrary binary embedding.
Concatenate raw bit strings, charging for both computed words.
Prepend a computed bit to a raw bit string.
Read the head of any list encoding with a fixed fallback.
Read a computed framed list's head, inferring the element encoding from the list before composing with a later field projection.
Drop the head of any list encoding.
Test emptiness without decoding a list element or requiring a default value.
Test a framed list's emptiness, determining its element encoding for automation.
Test a raw bit string's emptiness using the standard Boolean element encoding.
Drop the head of a framed list, determining its element encoding for automation.
Drop the first raw bit. The raw encoding fixes the otherwise undetermined element encoding.
Reverse a raw bit string using an accumulator that grows by one bit per step.
Prepend computed data. The result encoding determines the element encoding before
fun_prop searches for the two component certificates.
Concatenate computed lists, inferring their shared encoding from the result.
Reverse a framed list; the accumulator is a permutation of a prefix of the input.
Reverse a computed framed list, inferring its element encoding from the result.
Find the first element passing a polynomial-time test with a fixed parameter. The list may have any polynomial encoded length.
Search with a predicate that captures the original input.
Keep the elements passing a polynomial-time test with a fixed parameter. The input list may have any polynomial encoded length.
Filter with a predicate that captures the original input.
Filtering a list by a polynomial-time test is polynomial-time.
Map a polynomial-time function with a fixed parameter over a polynomial-time computable list. The list may have any polynomial encoded length.
Map a function that also uses the original input. A single joint certificate in the input
and list element makes the cost uniform across all elements. The list certificate is supplied
first so that fun_prop can infer its element encoding before checking the body.
A polynomial-time function can be mapped over a list in polynomial time.
Read an optional head in any list encoding, without an inhabitant of the element type.
Map an input-dependent function over a fixed list. Only its members need certificates; the list and its elements are not part of the computational input.
Concatenating a list of lists is polynomial-time.
Concatenate polynomial-time lists computed from each element and a fixed parameter.
Concatenate lists computed jointly from the original input and each list element.
Like mapWithInput, this is a composition rule for fun_prop.
Concatenate input-dependent lists indexed by a fixed list of parameters. No encoding of the fixed parameters is required.
Filter and map a fixed list using computed guards and outputs. No encoding of the fixed parameters is required; only members of the list need certificates.
The length of a list, in unary, including raw bit strings.
Length of a raw bit string.
The encoded input length, computed in unary by reading the input word.
Length of a computed raw bit string, fixing the intermediate encoding for proof search.
Registered after encoding_length so fun_prop first tries this rule on computed words.
Count predicate matches directly over any readable, size-bounded list encoding. The accumulator is a unary counter; the certificate does not construct a list of matches.
Count matches of a predicate that captures the original input. The count is in unary.
Count occurrences of a computed value using lawful Boolean equality.
Enumerate 0, …, n - 1, with the bound and the elements in unary.
Repeat a computed value a computed unary number of times, charging every copy and delimiter.
Scan any readable, size-bounded list encoding for a predicate match.
Test every element of any readable, size-bounded list encoding.
Test whether any element satisfies a polynomial-time predicate with a fixed parameter.
Test whether every element satisfies a polynomial-time predicate with a fixed parameter.
Test whether any list element satisfies a predicate that captures the original input.
Test whether every list element satisfies a predicate that captures the original input.
Test every element of a fixed list. Only its members need certificates; the list and its elements are fixed before the computational input and require no encoding.
Test whether any element of a fixed list satisfies its input-dependent predicate. The fixed list needs no element encoding or uniform certificate over all possible elements.
The index of the first occurrence, or the list length if absent, computed in unary. The element itself can use any encoding.
Find a computed value's first occurrence in a computed list.
Drop a unary number of elements from a sized list encoding, including raw bit strings.
Drop a computed unary number of elements from a computed framed list.
Take a unary number of framed-list elements using certified reversal and dropping.
Take a computed unary number of elements from a computed framed list.
Look up a computed unary index, returning none outside a computed list. The list certificate
determines its encoding before proof search checks the corresponding operation and size rules.
Drop a computed unary number of bits from a computed bit string.
Take a computed unary number of bits from a computed bit string.
List lookup with a fixed default and a unary index, including lookup in raw bit strings.
Read a bit at a unary index with a fixed fallback. Fixing the raw encoding avoids guessing a list-encoding instance during compositional proof search.
Read a computed bit string at a computed unary index.
Lookup in a computed list at a computed binary index. The index is first capped at the length of the list, reading its binary digits most significant first and capping every partial value, so an index far beyond the list costs only its binary length; beyond the list every lookup returns the default.
Number the entries of a framed list with unary indices, charging the list and every index.
Plain polynomial-time automation #
Test whether any list element satisfies a predicate that captures the original input.
Concatenate raw bit strings, charging for both computed words.
Take a computed unary number of bits from a computed bit string.
The encoded input length, computed in unary by reading the input word.
Filter with a predicate that captures the original input.
Filtering a list by a polynomial-time test is polynomial-time.
Map an input-dependent function over a fixed list. Only its members need certificates; the list and its elements are not part of the computational input.
Concatenate input-dependent lists indexed by a fixed list of parameters. No encoding of the fixed parameters is required; only members of the list need certificates.
Filter and map a fixed list using computed guards and outputs, preserving order and duplicates. No encoding of the fixed parameters is required; only members need certificates.
Repeat a computed value a computed unary number of times, charging every copy and delimiter.
Concatenate lists computed jointly from the original input and each list element.
Like mapWithInput, this is a composition rule for fun_prop.
Read the head of any list encoding with a fixed fallback.
Length of a raw bit string.
Count matches of a predicate that captures the original input. The count is in unary.
Read a computed framed list at a computed unary index with a fixed fallback, inferring the element encoding from the list.
Read a computed bit string at a computed unary index. Registered after listGetDWithInput so
fun_prop tries raw bit-string lookup before framed-list lookup on Bool.
Drop a computed unary number of bits from a computed raw word. Counts beyond the word length return the empty word, with no promise on the count or input.
Length of a computed raw word, fixing the intermediate encoding for proof search.
Find the first list element passing a test that captures the original input.
Count the list elements passing a test with a parameter, in unary.
Test whether some list element passes a test with a parameter.
Test whether every list element passes a test with a parameter.
Framing a fixed Boolean encoding, or parsing its frames and converting each symbol, takes
polynomial time. The encodings of false and true can be arbitrary fixed words.
The word conversion preserves an arbitrary caller-supplied encoding. No computable inverse
of encIn is assumed: expose its word, convert that word, and reuse the resulting encoding.