[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 23 Jun 2014 12:04:26 -0700 (PDT)

This is in response to the posting *Dictionary type*, but I thought

it merits a new topic.

Ordinary mathematics has no formal notion of a "partial function".

Mathematicians sometimes informally talk about a function that's not

defined on its entire domain. For example, they may talk about the

reciprocal function, which maps a number r in the set Real of real

numbers to 1/r, as a function on the set Real that's undefined on 0 or

"has a singularity at" 0. Formally, this just means that the domain

of the function is Real \ {0}.

The formal notion of a partial function arises in typed formalisms

with simple types. If the type system isn't expressive enough to

treat Real \ {0} as a type, then reciprocal must be defined to have

type [Real -> Real] that is a partial function because it's not

defined on all values of type Real. Since the customary formalism

of ordinary math doesn't use types, "partial function" has no

formal meaning.

Informally thinking of reciprocal as a function on Real that's not

defined on 0 may be useful. However, I see no benefit in thinking of

elements of DictionaryType as partial functions on STRING, when their

domain is such a "small" subset of STRING. You should be comfortable

with the idea that the domain of a function can be any set. No

mathematician would think of the element

[key1 |-> "value1", ..., keyN |-> "valueN"]

as a function on STRING that's undefined on any string in

STRING \ {"key1", ... , "keyN"}

You are better off learning to think like a mathematician. You can

formally define the reciprocal function to be either a function in

[Real \ {0} -> Real] or else a function in [Real -> Real] that maps

0 to some special value such as

NotANumber == CHOOSE n : n \notin Real

Either choice is fine. Depending on the nature of your spec, one

might be more convenient than the other. (As a more realistic

example, when specifying an algorithm, you might want to define

a function cdr on some set of sequences by

cdr[s] == IF s = << >> THEN nil ELSE Tail(s)

for a special value nil.)

By the way, in ordinary math, the two definitions of DictionaryType

that Dominik gave would be equal, since functions are defined to be

sets of ordered pairs and [S -> T] equals S \X T. TLA+ does not define

functions in terms of ordered pairs, the way mathematicians do,

because it's convenient to define an ordered pair (and any tuple) to

be a function. I could have defined a different type of pair--for

example by defining

Pair(a, b) == {{a}, {a, b}}

and defining [S -> T] to equal

{Pair(t[1], t[2]) : t \in S \X T}

Perhaps I should have done that, since it would have made f \cup g

a useful construct when (DOMAIN f) \cap (DOMAIN g) is empty.

However, instead I chose to make function-related operators like

DOMAIN primitives specified by axioms.

Leslie

**Follow-Ups**:**Re: "Partial" Functions***From:*Leslie Lamport

**Re: "Partial" Functions***From:*fl

- Prev by Date:
**Re: [tlaplus] Re: Dictionary type** - Next by Date:
**Re: [tlaplus] Parsing Error in Consensus.tla** - Previous by thread:
**Re: Parsing Error in Consensus.tla** - Next by thread:
**Re: "Partial" Functions** - Index(es):