Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: partial function

Bottom of Page

1 to 33 of 33

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeFeb 12th 2014

    added to partial function a new section Definition – General abstract with a brief paragraph on how partial functions form the Kleisli category of the maybe-monad.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 12th 2014

    That description of partial functions in terms of the monad 1+−1 + - works in SetSet, and (I think off the top of my head) in any Boolean topos, but not more generally.

    In the early days of topos theory, before the definition of topos became codified in the form best known today, people used to talk a lot about partial map classifiers. I haven’t checked to see what we have on that notion in the nLab.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2014

    In a general extensive category, the kleisli morphisms for the maybe monad will be the partial functions with complemented domain.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 12th 2014

    Yes, that’s the sharper way of putting it.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeFeb 12th 2014

    I had raised adding extensiveness in the other thread here.

    Will try to put it into the entry. Only have one hand free though…

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2014
    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 13th 2014

    There is already stuff about this monad (but the constructive version, not the maybe monad) near the bottom of the page, under “The category of sets and partial functions”. But this doesn't actually discuss how it's a monad!

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2014

    Ok, clearly partial function and partial map classifier and maybe monad need to be interlinked, and there is a query box from Emily on the former which should be answered. The “total functions S ⊥→T ⊥S_\bot\to T_\bot such that inhabited subsets of TT are assigned only to inhabited subsets of SS” referred to at partial function must be the algebra maps for the partial map classfier monad, so that we are identifying Set ⊥Set_\bot with the Kleisli category of that monad regarded as the subcategory of free algebras. However, it’s not immediately clear to me what a general algebra for this monad is in a constructive setting (classically, every such algebra is free).

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2014

    A type-theoretic description of the PMC as “the set of subsets with at most one element” is

    A ⊥=∑ P:A→PropisProp(∑ a:AP(a)). A_\bot = \sum_{P:A\to Prop} isProp\Big(\sum_{a:A} P(a)\Big).

    Am I right in thinking that this is equivalent to

    ∑ U:Prop(U→A)? \sum_{U:Prop} (U\to A) \quad ?

    If so, that at least gives a slightly more explicit description of its algebras.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 13th 2014

    I'm getting that those two expressions are describe equivalent sets in constructive set theory. If they both satisfy isSet in HoTT, then this means that they should be straight-up equivalent, yes?

    • CommentRowNumber11.
    • CommentAuthorZhen Lin
    • CommentTimeFeb 13th 2014

    Proposition 2.4.7 in [Sketches of an elephant, Part A] constructs the partial map classifier as Σ ΩΠ ⊤A\Sigma_{\Omega} \Pi_{\top} A, where ⊤:1→Ω\top : 1 \to \Omega is the generic subobject. I suppose in type-theoretic notation this is

    ∑ U:Prop∏ x:⊤(U)A\sum_{U : Prop} \prod_{x : \top (U)} A

    and since the fibre ⊤(U)\top (U) is just UU itself, this is the type you describe.

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 13th 2014

    I put in some reply to Emily.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2014

    Thanks Zhen! Toby, they are both sets as long as AA is, which is the case I was thinking of; otherwise the first is a set but the second is not. And I think the second is a more sensible PMC for non-sets.

    • CommentRowNumber14.
    • CommentAuthorspitters
    • CommentTimeFeb 14th 2014

    What happens if we do the same construction for this constructive maybe monad? [Sorry, I don’t have the time now, I may come back later.] Also in type theory one considers the partiality monad where uses the “r.e. propositions”, of course this can be generalized to other classes of propositions.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 15th 2014

    And I think the second is a more sensible PMC for non-sets.

    Agreed.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 24th 2014

    I’ve added a few more remarks to partial map classifier and partial function.

    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 24th 2014

    I don't understand this business about ‘the set of functions P→BP\to B whose domain PP is a subsingleton’. In particular, in classical mathematics, this describes a proper class! I know what it's supposed to mean, but I don't know any way to formalize it in a topos other than by turning it into the previous construction. Arguably, the proper way to formalize the previous construction in HoTT is to turn it into this, so there's not really a difference between them.

    We can describe both of these, to be sure. But they don't really seem different to me. Certainly not internally to a topos.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 25th 2014

    I was trying to describe the two different definitions I gave above in #9. They are equivalent, as they must be, but they are different definitions.

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 26th 2014

    I rewrote them so that they're more clearly in the language internal to a category. In particular, there's no quantification over arbitrary subsingleton objects, just subobjects of one terminal object.

    But if I start being too explicit about how this looks in the internal language, then they start looking very similar again. (What is the object of partial maps 1⇀B1 \rightharpoonup B? Well, it's the object of subobjects of 1×B1 \times B such that […], which is of course the same as the object of subobjects of BB such that [back to the first definition].) Maybe we should use an explicit reference to the dependent sum over the object of truth values?

  20. Added to partial map classifier a remark on B+1B+1 always classifying partial maps whose domain of definition is a decidable subset of the source.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2014

    @Toby: Sure, if you think that would make it clearer.

    • CommentRowNumber22.
    • CommentAuthorspitters
    • CommentTimeMar 8th 2014

    Added the use in type theory. I expect classifiers for different classes of partial maps have also been studied (open, closed domain …) But I do not know the references off hand.

    The server seems to be having problems.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeAug 27th 2015

    I added some stuff about the algebra of real-valued partial functions of one real variable, the one that's studied in high-school math, as analysed by Fred Richman.

    • CommentRowNumber24.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 28th 2015
    • (edited Aug 28th 2015)

    I fixed the incorrect statement in the section http://ncatlab.org/nlab/show/partial+function#in_terms_of_the_maybe_monad which used to say that the domain of the partial function corresponded to the preimage of the extra disjoint point!

    @Toby

    I also added a statement that feels ’more constructive’, but is not quite there:

    an element x∈Ax\in A is sent to *\ast by ϕ\phi if and only if the original partial function is undefined at xx.

    I’d rather make a positive statement like “a partial function is defined at xx iff the corresponding partial function sends xx to a value in B⊂M(B)B\subset M(B)” where MM is the Maybe monad, since one doesn’t need to define the Maybe monad as (−)∐*(-)\coprod \ast. Or we don’t even need to phrase it in terms of Maybe: I would guess that B⊂M(B)B \subset M(B) is not an iso, or perhaps that there is an element of M(B)M(B) disjoint from BB, is enough.

    EDIT: oh, this all seems to be subsumed later down the page, with Set ⊥Set_\bot, where what I wrote as M(B)M(B) is there called B ⊥B_\bot, and is actually worked out.

    • CommentRowNumber25.
    • CommentAuthorTobyBartels
    • CommentTimeAug 28th 2015

    I think that I made that phrasing better; you can't make it work constructively using that monad, but at least one can avoid double negations.

    • CommentRowNumber26.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 28th 2015

    Thanks Toby, that’s much better!

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeAug 28th 2015

    Thanks!

    • CommentRowNumber28.
    • CommentAuthorGuest
    • CommentTimeApr 23rd 2022

    The contents of category of partial functions in a set (homotopytypetheory) should be merged into this article.

  29. added section on partial functions in type theory

    Anonymous

    diff, v26, current

  30. removing query box from page:

    +– {: .query} Ronnie There is an interesting debate possible here!

    On the basis of my teaching of first year analysis and calculus since 1959, I found the most convenient idea is that of a function f:R→Rf: R \to R being a partial function with a domain which can be calculated from a formula for the function, and may be empty. Then one finds that the inverse of an injective function R→RR \to R is also a function R→RR \to R. A first order differential equation has a solution which is a partial function. What seems to be lacking is the functional analysis of such solutions. For example dy/dx=1/(λ+x)dy/dx=1/ (\lambda +x) has a solution whose domain varies with λ\lambda and ought to (and can be made to) vary continuously, including its open domain!

    The work of Charles Ehresmann is full of partial functions, derived from his strong interest in analysis and differential geometry, and local-to-global problems. So he developed for example the theory of pseudogroups, and contributed to inverse semigroups.

    A possible reason for the difficulties some have of accepting groupoids rather than groups is that groupoids have a partial composition, which is of course very intuitive when one thinks of composing journeys.

    In higher dimensional algebra one is dealing with algebraic structures whose domains are defined by geometric conditions.

    Of course category theory initially derived from algebra and algebraic topology, where partial functions are unusual. However they are necessary in dealing with fibred exponential laws, i.e. exponential laws in a slice category of TopTop, and their applications. See papers of Peter Booth.

    Toby: For first-year calculus, I agree with you, except that you ought to be able to restrict the definition to an interval (or a union of intervals) by fiat. (Actually, you can get this from formulas by adding appropriate terms of the form x−a−x−a\sqrt {x-a} - \sqrt{x-a}, log(a−x)−log(a−x)\log(a-x) - \log(a-x), etc, but that's silly.) So calculus is about (certain) functions to R\mathbf{R} from unions of intervals on R\mathbf{R}. Of course, this doesn't include all partial functions on R\mathbf{R}, but then it doesn't even include all such total functions, so maybe the restriction on allowed domains doesn't matter.

    But if you disagree that ’in more sophisticated analyses […], these domains and the total functions on them become the primary objects of study’, then feel free to change the text (say to ’in other analyses […]’; I don't intend to defend the claim that this is really the right way to do things. =–

    Anonymous

    diff, v26, current

  31. removing old query box

    +– {: .query} Emily Riehl I don’t understand how I am supposed to think about Set ⊥Set_\bot. In particular, Set ⊥Set_\bot is isomorphic to get category of based sets and basepoint preserving functions, which seems both easier to describe and easier to think about.

    Also what is non-constructive about the bijection S ⊥≅S⨿{⊥}S_\bot \cong S \amalg \{\bot\}?

    Toby writes: We have the map S⨿{⊥}→S ⊥S \amalg \{\bot\} \to S_\bot; map xx to {x}\{x\} and ⊥\bot to ∅\emptyset. Suppose that this map is surjective. That's fine for some SS, but suppose that SS is inhabited, with an element aa. Let PP be any proposition, and form the subset {x|P}\{x | P\} of SS, defined so that a∈{x|P}a \in \{x | P\} iff a=xa = x and PP is true. This subset has at most one element, so it is (by hypothesis) in the image of the map S⨿{⊥}→S ⊥S \amalg \{\bot\} \to S_\bot. If its preimage is in SS, then PP is true; if its preimage is in {⊥}\{\bot\}, then PP is false. Since PP could be any proposition, excluded middle follows; this is nonconstructive.

    This is all yet different from the category of pointed sets. =–

    Anonymous

    diff, v27, current

  32. added definitions of partial anafunctions in type theory and their relation to partial functions

    Anonymous

    diff, v28, current

  33. Added publication info and doi for Fred Richman reference:

    Anonymouse

    diff, v31, current

1 to 33 of 33

  1.