Skip to content

Native support of PCFs in identify #13

@itaybthl

Description

@itaybthl

The values array should be able to contain lib.pcf.PCF instances. When any PCF is included, first identify must check LIReC if its canonical form has any relations to a NamedConstant. If it does, terminate early and notify the user of the relevant NamedConstant(s) and the relation(s). Otherwise, compute the PCF to the desired minimum precision and then include it in the usual workflow of identify. However, warn the user if the PCF is predicted to have polynomial convergence, and add a max_cf_depth argument to identify that defaults to 2**20 and cuts off computation at max_cf_depth even if precision is not achieved, unless max_cf_depth=0 in which case this cutoff is disabled.
Also, once we add theorems on classes of PCFs (e.g. via CMFs), identify must check those as well before proceeding with any PCF it is given.
Finally, if any such PCF, checked through identify, is found to be connected to constants in LIReC, it must be automatically added as a PcfCanonicalConstant, or at least put on a special waiting list to independently verify by us. (most likely we will go with the waiting list)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions