English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We investigate partial functions and computability theory from within aconstructive, univalent type theory. The focus is on placing computability intoa larger mathematical context, rather than on a complete development ofcomputability theory. We begin with a treatment of partial functions, using thenotion of dominance, which is used in synthetic domain theory to discussclasses of partial maps. We relate this and other ideas from synthetic domaintheory to other approaches to partiality in type theory. We show that thenotion of dominance is difficult to apply in our setting: the set of$\Sigma_0^1$ propositions investigated by Rosolini form a dominance preciselyif a weak, but nevertheless unprovable, choice principle holds. To get aroundthis problem, we suggest an alternative notion of partial function we calldisciplined maps. In the presence of countable choice, this notion coincideswith Rosolini's.  Using a general notion of partial function, we take the first steps inconstructive computability theory. We do this both with computability asstructure, where we have direct access to programs; and with computability asproperty, where we must work in a program-invariant way. We demonstrate thedifference between these two approaches by showing how these approaches relateto facts about computability theory arising from topos-theoretic andtype-theoretic concerns. Finally, we tie the two threads together: assumingcountable choice and that all total functions $\mathbb{N}\to\mathbb{N}$ arecomputable (both of which hold in the effective topos), the Rosolini partialfunctions, the disciplined maps, and the computable partial functions allcoincide. We observe, however, that the class of all partial functions includesnon-computable partial functions.

Partial Functions and Recursion in Univalent Type Theory