2
$\begingroup$

I understand that functions are not defined in type theory the same way they are defined in set theory, hence functional property is not directly defined when defining function type in type theory. But I want to know which part of function type definition in type theory guarantees functional property even if it is done so indirectly and implicitly?

$\endgroup$
  • 1
    $\begingroup$ Try to write a function in a lambda-calculus that does not satisfy such a property ;-) ---the idea is that such a property is baked into the system, you need not check it. If you consdier a lambda calculus for continous functions, for example, then you need not check that the resulting functions are continous: The property is baked in ;-) $\endgroup$ – Musa Al-hassy Jun 11 at 19:22
  • $\begingroup$ Thanks Musa, I thought so but then it raises the question that isn’t type theory supposed to define everything through judgments and construction/elimination interplay? How come all of a sudden it brings in a sophisticated system like lambda calculus or formula into play from nowhere when it comes to defining function type?!! $\endgroup$ – al pal Jun 11 at 19:51
  • $\begingroup$ Also there is not a single mention of lambda calculus at all in Ituitionistic Type Theory by Martin-Lof! $\endgroup$ – al pal Jun 11 at 20:23
4
$\begingroup$

Type theory shows that every element of a function type has the "function property". Let $A$ be a type and $B(x)$ a dependent type with $x : A$. We can construct an element of $$\Pi (x : A) (y , z : B(x)) \,.\, f x =_{B(x)} y \to f x =_{B(x)} z \to y =_{B(x)} z$$ quite easily, because we just use symmetry and transitivity of equality. For instance in Coq:

Definition functional_property (A : Type) (B : A -> Type) (f : forall x, B x)
  : forall (x : A) (y z : B x) (p : f x = y) (q : f x = z),  y = z
  :=
   fun _ _ _ p q => eq_trans (eq_sym p) q.

What this means is that, as others already pointed out, the "functional property" is there by construction. It may help to say the following: in type theory we do not think of mathematical objects as existing independently and beforehand. Instead, type theory is a theory of how objects are constructed. Thus, the elements of the function type are constructed in a certain way (known as "$\lambda$-calculus") that guarantees the desired properties by construction. There is no such thing in type theory as "a thing that wants to be a function but isn't because it doesnt have the right properties". That sort of thinking simply does not apply: if you have a thing, then it was constructed according to the rules of some type and therefore the thing has that type.

You are probably thinking set-theoretically, i.e., given a relation $R \subseteq A \times B$, we should be able to get a function out of it, provided that $R$ is single-valued (what you call "functional property") and total. There is a corresponding statement in type theory, but it is not the definition of functions. It is instead a theorem stating that the function type $A \to B$ is equivalent to the type of total functional relations.

$\endgroup$
  • 1
    $\begingroup$ (In the displayed formula, at the end, it should be $y =_{B(x)} z$ instead of $x =_{B(x)} z$) $\endgroup$ – Ingo Blechschmidt Jun 12 at 13:48
  • $\begingroup$ @IngoBlechschmidt: yes, thanks. I fixed it. $\endgroup$ – Andrej Bauer Jun 12 at 21:03
3
$\begingroup$

Set theory does not have functions. Instead, we can model functions via special relations (i.e. sets of pairs). When we write $f(x)=y$ in a set-theoretic context, what this actually means is $(x,y)\in f$. If $f$ was an arbitrary binary relation, there would be absolutely nothing stopping $(x,y)\in f$ and $(x,y')\in f$ with $y\neq y'$. By definition of set-theoretic functions, this is not allowed, so when we propose that some relation is a set-theoretic function, we need to show that this does not happen (among other things).

(ZFC) Set theory is defined within first-order logic. It is typically defined so that the only non-logical symbol is the predicate symbol $\in$ (treating $=$ as a logical symbol). In particular, there are no function symbols. For first-order theories in general (in first-order logic with equality), part of the definition of equality is that it is substitutive with respect to predicates and terms. In particular, $x=y\implies f(x)=f(y)$ is either an axiom or readily derived from the logical axioms defining equality.

Again, the key thing here is that a function symbol, even in a set theory, is not the same thing as a set-theoretic function (and vice versa). It's interesting to consider what happens when equality isn't taken as part of the logical framework. Then it becomes an arbitrary binary predicate symbol and the statements about it imply that it is interpreted by an equivalence relation. Substitutivity then means, under interpretation, that $x\sim y\implies f(x)\sim f(y)$. A key thing here is that we only require substitutivity for formulas/terms that we can write down in the language of the theory.

The above was a bit of an aside to provide context. Type theory is not presented as a first-order theory like set theory. Instead, type theory is more like an alternative to first-order logic. Nevertheless, the handling of functions in type theory is more or less the same as how function symbols are handled in logic. Depending on the type theory, the issue either can't be articulated in any sensible manner, or, like for FOL, is more about properties of equality and to the extent that equality behaves as we'd expect, is trivially demonstrable.

None of this has much to do with function types in particular. The relevant claims for values of function types will follow, if the articulable at all, from substitutivity of equality with respect to the operations of the type theory. For example, if $f:B^A$ is a term of function type and $\mathsf{app}_{A,B}$ is the operation that performs function application, then substitutivity with respect to $\mathsf{app}_{A,B}$ will imply the analogous statement for values of function type. In other words, the fact that $\mathsf{app}_{A,B}(f,x)$ is a term (when $f:B^A$ and $x:A$) already implies functionality.

$\endgroup$
0
$\begingroup$

If I understand correctly what you mean by "functional property", the functional property of an inductive type A comes from its induction rule, that defines a function with domain A and codomain any type C of the "adequate form", together with computation rules, that define how the induction rule computes on all the possible constructors of A inhabitants.

$\endgroup$
  • $\begingroup$ By functional property I mean the fact that a function can not assign two different values to a single value of its domain. If that is what you described would you please provide me an example? $\endgroup$ – al pal Jun 11 at 21:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.