Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

It kind of depends on the formalism. In one setting you imagine a universe of things U and a function f maps its domain D < U to its range R < U. In other words, D and R are derived properties of the function, f.

On the other hand, you might define a function as a triple (D, R, f) which lets us discuss, and then immediately outlaw, the idea of a value x in D such that f(x) is not-defined.

The most flexible approach is, as stated, to define relations as subsets of DxR first and then take functions to be a specialized subset of relations. Then we have exact ideas for what happens when a function fails to map the entire (explicitly stated) domain and can talk about other cool concepts like restrictions.



What means D < U in your notation? It's like, D is a subset of U?

Anyway the problem with trying to make a function total by fiat like with the definition (D, R, f) is that for some functions (even computable functions), its domain may be an uncomputable set.

That's because if we could decide if a given x in f(x) makes f return something or not, if f represents the output of a Turing machine we could use that to solve the halting problem.

So while in principle every function is total in some domain D (precisely the domain which it is defined to return some value), sometimes we can't talk very usefully about this domain. In this case, we choose to treat f as a partial function and talk about a larger set of values D' f receive as input (and might or might not return anything), for which D is a subset.

Some properties might not be literally undecidable but we may not know how to solve them yet. For example, the function collatz : Nat -> () [0] that receives a natural number and either return nothing if its collatz sequence[1] eventually reaches 1, or else run forever. What's the domain of this function? (you can switch this for any actually undecidable problem for extra hardness)

Unfortunately the linked article doesn't talk about this particular motivation for defining partial functions in computer science, and instead cites sqrt as an example, even though it has a perfectly computable domain. The domain of sqrt is just the non-negative reals; which we could give a more precise type to sqrt in if we have means to define the type of non-negative numbers (maybe using the smart constructors[2] technique, available in any programming language that lets you to define records/structs), which may or may not be ergonomic. We don't need dependent types for that, but they could be a tool to make this stuff ergonomic and actually check this at compile time (first class support for refinement types would also help).

[0] something like this

    fn collatz(n: natural) {
        while (n != 1) {
            if n % 2 == 0 {
                n <- n / 2;
            }
            else {
                n <- 3*n + 1;
            }
        }
    }
[1] https://en.wikipedia.org/wiki/Collatz_conjecture

[2] https://markkarpov.com/post/smart-constructors-that-cannot-f...


> On the other hand, you might define a function as a triple (D, R, f)

That's also the approach in Functional Analysis. Depending on how you choose D and R, some fundamental properties of the function change, e.g. bijectivity. Therefore specifying the sets is strictly speaking not optional.

The proper function definition in the other formalism would be rather:

f: D -> R: ...




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: