Zulip Chat Archive

Stream: maths

Topic: Teaching functions


view this post on Zulip Gihan Marasingha (Oct 17 2020 at 16:45):

For those using Lean for teaching mathematics, how do you treat the notion of function?

Until this year, I've taught my beginning undergraduates that a function is a triple (A,B,C)(A, B, C) of sets where CA×BC \subseteq A \times B with the properties:

  1. aA,bB,(a,b)C\forall a \in A, \exists b \in B, (a,b) \in C and

  2. aA,b1b2B,(a,b1)C(a,b2)Cb1=b2\forall a \in A, \forall b_1 b_2 \in B, (a,b_1) \in C \land (a,b_2) \in C \to b_1 = b_2.

The type-theoretic notion of a function as a named lambda abstraction does away with the distinction between functions that have the same 'map' but different domains or codomains. I see that data.set.function provides, for example, inj_on to define what it means for a (type-theoretic) function to be injective on a set. But this moves the notion of domain of a function to the definition of injectivity, rather than treating it as part of the definition of the function. That's fine, but it isn't the same notion of function as that given above.

My question to those teaching undergraduate maths with Lean is: do you just work with the type-theoretic definition? If not, do you use inj_on to define injectivity, or do you do something else entirely?

view this post on Zulip Yury G. Kudryashov (Oct 17 2020 at 16:47):

In Lean each function knows its domain: f : α → β has domain α.

view this post on Zulip Yury G. Kudryashov (Oct 17 2020 at 16:47):

If we want to study this function on a subset of its domain, then we introduce an auxiliary s : set α and define docs#set.inj_on etc

view this post on Zulip Yury G. Kudryashov (Oct 17 2020 at 16:48):

docs#function.injective does not use any sets

view this post on Zulip Gihan Marasingha (Oct 17 2020 at 17:11):

OK, so is the best solution not to worry about the distinction between sets and types?

When we use inj_on to look at a function on a subset of its domain, then the new domain is not part of the function, but has been moved into the position of being an argument of inj_on. To me, this is a different definition of function than that which I'm used to, but I accept that it's the most natural definition as far as Lean is concerned.

My view would be that α and β aren't domains and codomains in the traditional sense, as they aren't sets. Rather, to reconcile with the set-theoretic notion of function, a function would consist of a triple A : set α, B : set β, C : set α × β with the above properties, but this seems overly complicated and hard to work with in Lean.

view this post on Zulip Reid Barton (Oct 17 2020 at 17:12):

For most (math) purposes the correct mapping is "set" = Type, "subset" = set

view this post on Zulip Floris van Doorn (Oct 17 2020 at 17:12):

When I explain functions, I like to explain that a function is a mathematical procedure that takes a certain class of inputs to an output. A function "knows" what its inputs can be (its domain), and what its potential outputs can be (its codomain).

The definition you gave is an encoding of that idea in set theory. I don't think what you wrote has to be the definition, it just the most convenient encoding of the mathematical idea of a function in set theory. In type theory there is a different encoding (which is hardly an encoding, since functions are a primitive notion in type theory).

The idea that functions have the same 'map' but different domains and codomains looks a little different in type theory than in set theory, but you can find analogues of everything in one theory in the other theory. In type theory, two maps cannot be "the same" without having the same domain and codomain, but I don't think that is an essential feature of function.
If you have A → B and C ⊆ A you can still restrict your function to C in both set theory and type theory. In set theory, the "map" of your new function will be a subset, in type theory it will use subtype.rec, if we encode C as a subtype of A.

view this post on Zulip Reid Barton (Oct 17 2020 at 17:13):

e.g. "A group is a set GG equipped with a binary operation m:G×GGm : G \times G \to G and ..." -> (G : Type) (m : G -> G -> G)
"A subgroup HH of a group GG is a subset HGH \subset G such that ..." -> (H : set G) ...

view this post on Zulip Reid Barton (Oct 17 2020 at 17:16):

(This works better with a "structural" idea of what a set is, e.g., "an object of the category of sets", rather than a "material" one as in a set theory like ZFC)

view this post on Zulip Gihan Marasingha (Oct 17 2020 at 17:19):

Thanks everyone. That makes sense and will save a lot of faffing about. I suspect students will find the type-theoretic notion to be more natural that the set-theoretic one anyway.

view this post on Zulip Patrick Massot (Oct 17 2020 at 17:47):

@Gihan Marasingha did you have a look at the tutorials project? It's almost only a translation into English of the Lean files I use with first year undergrads (double major in math and computer science). The only differences are a couple of efficiency optimizations (saving a couple of lines of Lean code using rintros instead of intros followed by cases, things like that). The question you asked here simply do not arise. Functions in (dependent) type theory is just way closer to actual mathematical intuition that the set theory bullshit we sometimes have to pretend to believe when teaching.

view this post on Zulip Yury G. Kudryashov (Oct 17 2020 at 17:47):

E.g., the type-theoretic notion corresponds to function types in programming languages:

double sqr (double x) { return x * x; }

corresponds to

def sqr : double  double := λ x, x * x

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 18:33):

Floris said

When I explain functions, I like to explain that a function is a mathematical procedure that takes a certain class of inputs to an output. A function "knows" what its inputs can be (its domain), and what its potential outputs can be (its codomain).

I shy away from saying exactly what kind of procedure it is -- if I prove that for all f :R -> R, if f is differentiable then it is continuous, the f in that argument is not something defined by a mathematical procedure

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 18:36):

But just to add to the chorus Gihan -- the A and B you have in your definition are definitely types in Lean. All the intuition goes through.

view this post on Zulip Gihan Marasingha (Oct 17 2020 at 19:12):

@Patrick Massot yes, I really enjoyed the tutorial project! I learned much about Lean (including rintros) from it. Fortunately, my high-school French was sufficient to understand the only text that remained untranslated: "Ce n'est pas cela. Essayez encore".

@Kevin Buzzard: according to Liebeck, 'A function from SS to TT is a rule that assigns to each sSs \in S a single element of TT'. Is 'rule' different from 'procedure' or has M1F changed since the 1990s? ;)

All: I like the type-theoretic approach and I agree that it's more natural in many ways (the definition of function being a case in point) than the set-theoretic approach. I'm lucky to have the freedom to try this, but not all of my colleagues are sold on teaching mathematics formally (one said 'Buzzard can do this at Imperial, but...'). That's one of the reasons for raising the set / type issue as it relates to functions.

I hope others will come round eventually. This is reminiscent of the Bourbaki-influenced changes in teaching last century.

view this post on Zulip Johan Commelin (Oct 17 2020 at 19:19):

People are still bashing Bourbaki, right?

view this post on Zulip Patrick Massot (Oct 17 2020 at 20:20):

Gihan Marasingha said:

yes, I really enjoyed the tutorial project! I learned much about Lean (including rintros) from it. Fortunately, my high-school French was sufficient to understand the only text that remained untranslated: "Ce n'est pas cela. Essayez encore".

Good catch! I just translated it. But really, the message is that good (but not elite) first year students can handle those exercises.

view this post on Zulip Patrick Massot (Oct 17 2020 at 20:21):

Gihan Marasingha said:

I'm lucky to have the freedom to try this, but not all of my colleagues are sold on teaching mathematics formally (one said 'Buzzard can do this at Imperial, but...').

You can tell them "Massot can do that at Orsay too".

view this post on Zulip Patrick Massot (Oct 17 2020 at 20:23):

Actually I use Lean for teaching much more than Kevin since I have 50 students each year which have a mandatory mathematics course using Lean.

view this post on Zulip Patrick Massot (Oct 17 2020 at 20:24):

Johan Commelin said:

People are still bashing Bourbaki, right?

Some people like to do that, but they will never undo the effect that Bourbaki had on mathematics.


Last updated: May 09 2021 at 11:09 UTC