Email Gateway (Aug 18 2022 at 18:37): Email Gateway (Aug 18 2022 at 18:37):From: Tobias Nipkow <nipkow@in.tum.de>
Am 04/11/2011 17:55, schrieb Lawrence Paulson:
Some of the other points that you mention relate to basic lambda-calculus. There is no need to study the lambda calculus in its full glory, as it is quite irrelevant to higher-order logic. Lambda-notation merely expresses the notion of a function, something that is curiously lacking in standard mathematical practice.
Actually, "x |-> e" is often used, and I wish Church had adopted it,
that would make it unnecessary to explain to a mathematician what this
lambda means. But you are right that the |-> notation is not really a
first-class citizen in mathematics.
Tobias
The type of the composition operator is a well-known device, known as currying, for expressing functions that take multiple arguments. Again, traditional mathematics is quite careless in such situations. You remark that functions have domains and ranges, but typically the function composition operator is not written in such terms at all, and is allowed to apply to any compatible pairs of functions whatever. In the language of set theory, it is a class function.
Anything that you can define in higher-order logic is not merely explicable in traditional mathematical terms, but it is easily so. But there are plenty of things you can write in mathematics that are impossible to formalise in higher-order logic. This is because mathematics is essentially open-ended.
Larry Paulson
On 3 Nov 2011, at 18:45, James Frank wrote:
I'll ask the easy question first. In my inbox, there's isabelle-users@cl.cam.ac.uk and cl-isabelle-users@lists.cam.ac.uk . Does it make any difference which address I use to send in a question? If it doesn't, you don't need to answer that question.
I've tried not to ask different forms of my next question. That's because after studying enough type theory, lambda calculus, functional programming, and files from ~~/src/HOL, I'll figure out most of the answers. But that could be up to a years worth of work, and I'm trying to get a feel for where this road is going, and whether I may need to travel the road less traveled.
My question, stated very general, is this: "Can I take a file such as ~~/src/HOL/Fun.thy, rephrase the definitions in the language of standard math definitions and theorems, with a few changes to accommodate types, and have these standard definitions/theorems be describing the same objects as the Isabelle definitions and lemma?" I'm not talking about starting with a different logical framework or set of axioms, and ending up at the same place.
Below I ask related questions which are probably more straight forward to answer, and, if answered, might answer the question just posed.
To get more specific, I'll ask some questions about "definition comp" in Fun.thy, which is the definition of function composition.
First, here are some related goals to set the context, for why I'm thinking about this now:
1) I want to cater to mathematicians who are doing traditional mathematics. Therefore, the language of my definitions and theorems needs to be reasonably familiar to them. I'd like to start rephrasing Isabelle defs and thms now.
2) I want to build on, and learn from, what others have done. Therefore, my first choice is HOL rather than ZF, since the library is larger, even though HOL is not as "traditional".Here's the definition of comp from Fun.thy:
definition comp :: "('b => 'c) => ('a => 'b) => 'a => 'c" (infixl "o" 55) where
"f o g = (\<lambda>x. f (g x))"Studying Haskell is what led me to Isabelle, and I studied just enough functional programming to know that comp is a function that takes type "('b => 'c)" and returns type (('a => 'b) => 'a => 'c)). I guess that's right, although I ask below about (\<lambda>x. f (g x)), and about its domain and range.
Functions have domains and ranges. You won't be surprised here, but never once have I seen "function composition" be defined with the domain being a set of functions, and the range being a set of functions whose elements are functions, which take functions, and return functions.
Here's what I want out of "definition comp", using more standard math language:
DEFINITION 1.1.1 (comp). Let g:'a-->'b and f:'b-->'c. Then (f o g):'a-->'b, where (f o g)(x) = f(g(x)).
Notice that I tweak the definition to use types rather than sets. I was also tempted to stick "(f o g) = (%x. f(g x))" in there, not that I know much more than what it symbolizes. The details and groundwork could be worked out if it's basically the same thing as "comp".
A pertinent point here is that with a definition such as DEFINITION 1.1.1, I'm not making many demands on someone. They might be willing to go with it even with only an intuitive understanding of types and lambda calculus. However, it's important to me that something like DEFINITION 1.1.1 and "comp" be the same thing. Not be like, "think of them as the same", but "are the same".
Okay, what I really want is something like this:
(f o g) = {(a,c) in AxC | ThereExists b in B, such that (a,b) is in g and (b,c) is in f}.You can tell me different, but I assume I'm correct in saying that "comp" is not this set, and can't be this set, though with some work, some form of equivalence could be shown. Again, I guess that's right.
Somewhere in this question is me trying to figure out how different "comp" is from a standard definition of composition. Is "comp" close enough to a standard definition to try and phrase it using standard language, or it's "functional programming, type theory, and lambda calculus", and I should just accept it for what it is. Regardless, it is what it is, and I want to describe it as what it is, but describe it using language other than Isabelle code.
POINT 1: In a standard definition of function composition, there are typically three functions, "f", "g", and "f o g".
POINT2: In "comp", there are four functions, "f", "g", "(\<lambda>x. f (g x))", and the function of type
"('b => 'c) => ('a => 'b) => 'a => 'c".What I've said above might could be summarized with this question:
What is this thing, this function "('b => 'c) => ('a => 'b) => 'a => 'c"?If I have to incorporate that into my traditional-style definition, then it's no longer traditional-style. If I have to do that, then I'm doing something different.
If it's necessary details, and a way of specifying "g:'a-->'b, f:'b-->'c, and (f o g):'a-->'b", and I can easily formalize the connection prior to my function composition definition, then the situation is salvageable.
Anyway, feel free to comment or not.
Thanks,
James
Email Gateway (Aug 18 2022 at 18:38):From: Ramana Kumar <rk436@cam.ac.uk>
On Fri, Nov 4, 2011 at 5:46 PM, James Frank <james.isa@gmx.com> wrote:
Have you seen it [composition] being defined as a function before? If so, what was
its domain and range?(I also want to ask: how would you usually think of an ordinary
function that takes two arguments? This line would continue into a
discussion about currying, but I'll leave it out for now.)I could restate the essence of my first email: Currying is not a problem. It
not being a part of the math literature is a problem. I don't understand
currying because I wasn't taught currying. My math professors didn't teach
me currying because they didn't understand currying. Most likely, they were
very happy knowing nothing about currying. Most likely, they will die happy
knowing nothing about currying. That's not a problem unless I want them to
read something that I write that involves currying, but I will, or someone
like them, so it's a problem.
It's not too hard. I would encourage you to answer my two questions above.
For example, when I use "comp f g" in my mind rather than "f o g", it gives
me better understanding.
I agree. (That's why I like Lisp's syntax, or rather, lack of syntax.)
I think I had figured out that the whole thing,
"('b => 'c) => ('a => 'b) => 'a => 'c"
is (%x. f(g x)), or "f o g", though initially I was mistaking (%x. f(g x))
for the function of type ('a => `c), since in a traditional definition if
g:A-->B and f: B-->C, then (f o g):A-->C.
You got it right the first time. The type of (%x. f (g x)) is 'a => 'c.
But if "f" is the function of type ('b => 'c), "g" is the function of type
('a => 'b), and (%x. f(g x)) is the function of type "('b => 'c) => ('a
=> 'b) => 'a => 'c", then who is that function of type ('a => `c)?
Since "%x. f (g x)" is the function of type 'a => 'c (and it is equal
by definition to "f o g"), the question should perhaps be what is the
function of type "('b => 'c) => ('a => 'b) => 'a => 'c"? And the
answer, as I mentioned before, is "comp". Let's see how this works in
full detail.
We have the following typings
f :: 'b => 'c
g :: 'a => 'b
comp :: ('b => 'c) => ('a => 'b) => 'a => 'c
therefore
comp f :: ('a => 'b) => 'a => 'c
and thus
comp f g :: 'a => 'c
Done. For extra practice, consider the definition of "comp f g".
It was given as "%x. f (g x)", and we now know that it is a function
of type 'a => 'c.
That means "x" has type 'a, and f (g x) has type 'c.
And indeed that checks out:
x :: 'a, so
g x :: 'b, so
f (g x) :: 'c
Email Gateway (Aug 18 2022 at 18:38):From: James Frank <james.isa@gmx.com>
I'm not used to using "reply all", so I put this back public, along with
my previous response, where I admit that it's pretty foolish to be
wanting to eliminate something that's at the core. After this set, I
don't want to be so guilty of cluttering up the mailing list with
non-technical emails.
On 11/4/2011 6:13 PM, Lawrence Paulson wrote:
On 4 Nov 2011, at 19:31, James Frank wrote:
The problem is with this ubiquitous "'a => 'b => 'c" type statement. It's not a part of 98% (a little less or little more) of the math world.
I can't believe that any serious mathematician would struggle with this.Larry Paulson
It never entered my mind that they couldn't understand it, it's my
assumption that they don't even want to, especially not for me.
But that's an assumption for my purposes. You're Larry Paulson at
Cambridge. You make waves. I ride waves. The only safe assumption for me
is that no one is going to learn functional programming concepts for me.
We try and cater to the reader, some of us more than others. I'm trying
to set myself up now to do that in the future. I see the HOL wave and
the ZF wave. The HOL wave is bigger, and I want the potential support
and opportunity that may come with it, so I initially pick the HOL wave.
But you make it sound simple, this transition to math heavily tied into
functional programming. It's not that some of the basic concepts are
rocket science, but where's the satisfaction in just having a basic,
intuitive understanding of concepts? Having that attitude goes against
the very core of seeking to justify everything in math.
And then there's always the person who wants to take it to the next
level. It's not enough for him or her to do algebra, he or she has to go
wild with categories, and make me do lots of searches to find a decent
textbook on categories for self-study, when algebra is perfectly fine
without another level of abstraction.
It sounds like I'm lecturing. It's not really my place to do that here,
but, obviously, I'm willing to do it.
--James
Dr. Paulson,
There is a sense in which your question is not entirely meaningful...
I can see that. It would be like me saying, "That epsilon in the
definition of limit is annoying me, because it annoys my students, and
they don't want to learn about epsilons. What's an easy way for me to
get rid of it?"
But the realization that I was going to commit some "rigor sins" is what
brought this on.
The basic idea is that I have two parallel lines of language in a
document. Standard "math English", and the Isabelle code. The purpose is
to help me clarify ideas, and to make the math more interesting and
appealing to a typical mathematician.
There's not a problem with something like "lemma interior_ball:
"x:interior S <-> (EX e>0. ball x e <= interior S)".
The problem is with this ubiquitous "'a => 'b => 'c" type statement.
It's not a part of 98% (a little less or little more) of the math world.
Initially, I thought, "Okay, mask it with some other notation if you
can, or talk about how, all together, the Isabelle code is equivalent to
my math English".
I realized I can't do that. When I get to qed, I want to say, "Look,
I've proved my math English theorem with Isabelle code." But if my math
English is not a reasonable mirror of the Isabelle code, then I haven't
proved anything but the Isabelle code.
It's not a real problem. I either broach a subject and give rigorous or
semi-rigorous explanations, or I use certain math without explaining
what I'm doing, and let the reader figure it out.
It's just that every analysis book in the world has a token introduction
to set theory, functions, etc.. With math, I'm an imitator, and easily
following that pattern is blown out of the water with HOL.
Anything that you can define in higher-order logic is not merely
explicable in traditional mathematical terms, but it is easily so. But
there are plenty of things you can write in mathematics that are
impossible to formalise in higher-order logic.
The good news is that different foundations converge at a higher point
where they a lot of math in common.
Again, there's no real problem. Very few people have an in-depth
understanding of the foundations of math, so there's a lot of skipping
that low level stuff anyway, or totally ignoring it.
--James
On 11/4/2011 11:55 AM, Lawrence Paulson wrote:
There is a sense in which your question is not entirely meaningful,
because you're asking whether rigorous but informal mathematics is
adequately captured by a particular formalisation, and such issues are
ultimately subjective. However, traditional mathematics is often assumed
to be based on set theory, and higher-order logic has very
straightforward models in set theory. In particular, if you look at the
function f o g, then you get exactly the same set of ordered pairs by
either route, assuming you're in the mood to interpret a function as a
set of ordered pairs. The situation with higher-order logic is very
different from that presented by various constructive type theories you
may have seen, where you typically cannot regard a function as a set of
pairs.
Some of the other points that you mention relate to basic
lambda-calculus. There is no need to study the lambda calculus in its
full glory, as it is quite irrelevant to higher-order logic.
Lambda-notation merely expresses the notion of a function, something
that is curiously lacking in standard mathematical practice. The type of
the composition operator is a well-known device, known as currying, for
expressing functions that take multiple arguments. Again, traditional
mathematics is quite careless in such situations. You remark that
functions have domains and ranges, but typically the function
composition operator is not written in such terms at all, and is allowed
to apply to any compatible pairs of functions whatever. In the language
of set theory, it is a class function.
Anything that you can define in higher-order logic is not merely
explicable in traditional mathematical terms, but it is easily so. But
there are plenty of things you can write in mathematics that are
impossible to formalise in higher-order logic. This is because
mathematics is essentially open-ended.
Larry Paulson
On 3 Nov 2011, at 18:45, James Frank wrote:
I'll ask the easy question first. In my inbox, there's
isabelle-users@cl.cam.ac.uk and cl-isabelle-users@lists.cam.ac.uk . Does
it make any difference which address I use to send in a question? If it
doesn't, you don't need to answer that question.
I've tried not to ask different forms of my next question. That's
because after studying enough type theory, lambda calculus, functional
programming, and files from ~~/src/HOL, I'll figure out most of the
answers. But that could be up to a years worth of work, and I'm trying
to get a feel for where this road is going, and whether I may need to
travel the road less traveled.
My question, stated very general, is this: "Can I take a file such as
~~/src/HOL/Fun.thy, rephrase the definitions in the language of standard
math definitions and theorems, with a few changes to accommodate types,
and have these standard definitions/theorems be describing the same
objects as the Isabelle definitions and lemma?" I'm not talking about
starting with a different logical framework or set of axioms, and ending
up at the same place.
Below I ask related questions which are probably more straight forward
to answer, and, if answered, might answer the question just posed.
To get more specific, I'll ask some questions about "definition comp" in
Fun.thy, which is the definition of function composition.
First, here are some related goals to set the context, for why I'm
thinking about this now:
1) I want to cater to mathematicians who are doing traditional
mathematics. Therefore, the language of my definitions and theorems
needs to be reasonably familiar to them. I'd like to start rephrasing
Isabelle defs and thms now.
2) I want to build on, and learn from, what others have done. Therefore,
my first choice is HOL rather than ZF, since the library is larger, even
though HOL is not as "traditional".
Here's the definition of comp from Fun.thy:
definition comp :: "('b => 'c) => ('a => 'b) => 'a => 'c"
(infixl "o" 55) where
"f o g = (\<lambda>x. f (g x))"
Studying Haskell is what led me to Isabelle, and I studied just enough
functional programming to know that comp is a function that takes type
"('b => 'c)" and returns type (('a => 'b) => 'a => 'c)). I guess
that's right, although I ask below about (\<lambda>x. f (g x)), and
about its domain and range.
Functions have domains and ranges. You won't be surprised here, but
never once have I seen "function composition" be defined with the domain
being a set of functions, and the range being a set of functions whose
elements are functions, which take functions, and return functions.
Here's what I want out of "definition comp", using more standard math
language:
DEFINITION 1.1.1 (comp). Let g:'a-->'b and f:'b-->'c. Then (f o
g):'a-->'b, where (f o g)(x) = f(g(x)).
Notice that I tweak the definition to use types rather than sets. I was
also tempted to stick "(f o g) = (%x. f(g x))" in there, not that I know
much more than what it symbolizes. The details and groundwork could be
worked out if it's basically the same thing as "comp".
A pertinent point here is that with a definition such as DEFINITION
1.1.1, I'm not making many demands on someone. They might be willing to
go with it even with only an intuitive understanding of types and lambda
calculus. However, it's important to me that something like DEFINITION
1.1.1 and "comp" be the same thing. Not be like, "think of them as the
same", but "are the same".
Okay, what I really want
[message truncated]
Email Gateway (Aug 18 2022 at 18:38):From: Steven Obua <steven.obua@googlemail.com>
Hi James,
you might be interested in following the progress of the "ProofPeer" (www.proofpeer.com) project which aims to build a cloud-based interactive theorem proving system. I hope that until the end of November a first prototype will be up and running that can be played with. You can already sign-up for it and login now, but not do much else.
We were also faced with the question which language / logic to use for ProofPeer. In the end we settled for Higher-Order Logic Set Theory as a logic, and a functional programming language inspired by Standard ML, Scala and Isabelle/Isar.
I think every serious mathematician will (want to) learn some pieces of higher-order logic and functional programming. At the same time, ZF set theory is a very flexible and elegant tool, and, as you pointed out, is familiar to all mathematicians. Our version of Higher-Order Set Theory provides a framework where you work in set theory most of the time and whenever you can, only becoming aware of and employing higher-order logic when you reach the boundaries of what can be done in a straightforward and comfortable way in ZF set theory.
Cheers,
Steven Obua
Email Gateway (Aug 18 2022 at 18:38):From: James Frank <james.isa@gmx.com>
Ramana,
Thanks for answering anyway, but this shows that a big part of the
battle is getting the notation down. At least I was right that there are
4 functions instead of 3 (though I was actually wrong in the total
number, as I discovered below).
I'm not used to a character that's been defined as an operator being
used by itself to refer to a function. Even now, I know I can talk of
"comp", but I don't know if I can talk of "o" without using it with f
and g. In Haskell I can refer to + by putting it in (+). All this would
feel second nature if I had been doing much coding and using functions
like sum(a,b) instead of "a+b".
That's all notation, it's six of one, or a half dozen of the other.
However, there's "comp", "comp f", and "comp f g", and those variations
are related to currying and the nifty things currying allows you to do
when defining other functions with "comp", as I understand it.
First, I don't know how to use "comp f g x", where to put the
parentheses, but that's trivial, and shows I haven't worked far enough
into the basic tutorials.
More importantly, I'm trying to figure out what the simple analogy is
between set based function composition and functional programming
function composition. My short answer guess is, "There is no simple
analogy to be made using the set function composition notation and the
functional programming function composition notation". Yes, they
accomplish the same thing, but no, they're not close enough. Their
notational similarities will hurt you and make a fool out of you.
Currying allows me to specify 3 related functions, "comp", "comp f", and
"comp f g". Wait. I need a fourth function which involves a variable...
But, no, it's even worse, now that I've studied your comments below
more. You listed five functions:
f :: 'b => 'c
g :: 'a => 'b
comp :: ('b => 'c) => ('a => 'b) => 'a => 'c
comp f :: ('a => 'b) => 'a => 'c
comp f g :: 'a => 'c
But that's helpful, along with comment on following the "type path". I
think it's a little clearer now that the lambda notation is just a way
to specify the path that x::`a follows when used as an argument for g.
It's currying. It can't be something else. That's why you guys
immediately tied my questions into currying.
But now, to answer your two questions:
_Q1_: Have you seen it [composition] being defined as a function before? If so, what was
its domain and range?
It's always defined as a function, where a function is a set of ordered pairs. If g:A-->B and f:B-->C, then the domain and range are determined for (f o g). We have to have (f o g):A-->C, where A, B, and C can be any sets.
_Q2_:(I also want to ask: how would you usually think of an ordinary function that takes two arguments? This line would continue into a discussion about currying, but I'll leave it out for now.)
As a two variable function f(x,y).
But it's not acceptable for me to think like that now. When I was studying functional programming for practical reasons, it was acceptable to think of "f: 'a => 'b => 'c" as a two variable function f(a,b), but once you make it part of a math definition, I'm only allowed to to think of it as what it is.
The only option is to set up an equivalence that allows me to think the way I want to think.
Thanks for the help,
--James
Email Gateway (Aug 18 2022 at 18:38):From: James Frank <james.isa@gmx.com>
Again, I didn't hit the right reply button on a previous reply, so I put
this back public. In my reply to Piotr, I said complementary things
about both Mizar and Isabelle. Personally, I'd like to learn all the
proof assistants, just for the fun of it.
Email Gateway (Aug 18 2022 at 18:38):From: Josef Urban <josef.urban@gmail.com>
Hi,
Piotr Rudnicki forwarded this thread, here is my view.
I have seen the following justifications of doing formal
mathematics in simply typed HOL instead of in standard set theory:
I do not think any of them is particularly valid today. It seems
to me that they are just deeply embedded in the LCF heritage (use
of ML, etc.). Larry himself has formalized ZF quite far in Isabelle.
ad (1): Automation of type inference in existing HOL-based
systems based on Hindley-Milner is quite simple in comparison to
dependent type systems, be it done foundationally as in Coq, or
as a soft type system as in Mizar. Additional type class
systems (in Isabelle and Coq) are themselves soft type systems
grafted on top of the systems' foundational cores, already
motivated by user demand for improved (non-foundational)
type-related automations.
ad (2): Automation of working with (not just total) functions is
again a fairly simple mechanism, implementable also in set
theory.
I think that any of the major systems (starting with Isabelle)
has today integrated much more powerful automations, based on
bridges to automated tools working in propositional and
first-order (not higher-order) logic, and its decidable
fragments.
I believe that the focus on total functions as foundational
objects came from their success in programming, but it is foreign
to most of mathematics as done by mathematicians. The
set-theoretical world of HOL is different from standard set
theory. Basic set-theoretical cosnstructs like von Neuman's
ordinals do not work for HOL's standard "sets" because of the
type constraints. The universe is sparser, because its sets are
typed. When I see a set-theory-related development done
in (Isabelle/)HOL (last time this was measure theory), it leaves
me wondering about how/if various set-theoretical agendas and
their implications (e.g. the forcing methods, implications of the
axiom of choice) are answered.
To sum up: I do not think that there are good pragmatic
automation-related reasons for persuading mathematicians to work
in HOL instead of ZF. Given the very low penetration that formal
mathematics has so far among mathematicians, I think it would not
hurt the formal systems to go where the mathematicians are.
Josef
Email Gateway (Aug 18 2022 at 18:38):From: Serguei Mokhov <serguei@gmail.com>
James,
JFYI, perhaps you should bring up some of these questions on the
Foundations of Mathematics (FOM) mailing list to get some of the
insight from the "other side" and see what they have to say about HOL
and FOM.
http://www.cs.nyu.edu/mailman/listinfo/fom
-s
Email Gateway (Aug 18 2022 at 18:39):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Unfortunately "where the mathematicians are" is to use language in a way
which is typical of natural languages, which contain exactly the sort of
inconsistencies and ambiguities which lead people to use formal systems
instead.
For example, mathematicians say things like "the derivative of f(x)",
when they are referring to the derivative of f, and they say f(n) =
O(g(n)) (but that O(g(n)) is a set of functions), when they mean f is
_in the set_ O(g) - etc.
Jeremy
Email Gateway (Aug 18 2022 at 18:39):From: Ramana Kumar <rk436@cam.ac.uk>
On Sat, Nov 5, 2011 at 5:21 PM, James Frank <james.isa@gmx.com> wrote:
I'm not used to a character that's been defined as an operator being used by
itself to refer to a function. Even now, I know I can talk of "comp", but I
don't know if I can talk of "o" without using it with f and g. In Haskell I
can refer to + by putting it in (+). All this would feel second nature if I
had been doing much coding and using functions like sum(a,b) instead of
"a+b".That's all notation, it's six of one, or a half dozen of the other.
You're right, it's just syntax. You can talk about o on its own by
putting it in brackets (o), just like + in Haskell. (o) is the same
thing as comp.
_Q1_: Have you seen it [composition] being defined as a function before? If
so, what was
its domain and range?It's always defined as a function, where a function is a set of ordered
pairs. If g:A-->B and f:B-->C, then the domain and range are determined for
(f o g). We have to have (f o g):A-->C, where A, B, and C can be any sets.
No. I was asking whether you'd seen composition itself, just the (o),
defined as a function before. You're saying that the result of
composition, f o g, is always a function. That's right. But I guess
usually you would think of the "o" there as an operator that can never
appear on its own without two arguments around it. From the
higher-order perspective, as you've noticed, all of these are
functions: "_ o _", "f o _", "_ o g", and "f o g". The first one takes
two functions and returns a function. The second two take one function
and return a function. The last one takes something (maybe not a
function, depends on g) and returns something else (again, depends on
f).
_Q2_:(I also want to ask: how would you usually think of an ordinary
function that takes two arguments? This line would continue into a
discussion about currying, but I'll leave it out for now.)As a two variable function f(x,y).
But it's not acceptable for me to think like that now. When I was studying
functional programming for practical reasons, it was acceptable to think of
"f: 'a => 'b => 'c" as a two variable function f(a,b), but once you make
it part of a math definition, I'm only allowed to to think of it as what it
is.
There are at least three ways to think about functions of multiple arguments.
1) Have a new variation on the theme of "function" for every number of
arguments it might take, so a function of two arguments is a different
although similar kind of entity as a function of one argument. It
might be a set of triples as opposed to a set of pairs, for example.
2) (Curried functions) Every function takes exactly one argument. To
get the effect of taking more arguments, return a function to consume
the remaining arguments. For example, suppose we have f(x,y) = x + y.
As a curried function, f would have type num => num => num, or, for
clarity, num => (num => num). When you apply it to one argument, it
returns a function of type num => num. Thus f 3 :: num => num. Now if
you apply that resulting function to one argument, it returns a
number. (f 3) 4 :: num (and (f 3) 4 = 7). We would usually write f 3 4
for (f 3) 4, by making function application associate to the left.
3) Every function takes exactly one argument. To get the effect of
taking more arguments, take all your required arguments at once in a
tuple. The function f as above would in this case have type num * num
=> num. You apply it to a pair of numbers (3,4), and get back a number
f (3,4) = 7.
Representations 2 and 3 are closely related. Indeed, you can write a
(higher-order) function to transform a curried function into an
uncurried function (and vice versa).
Are any of these close to how you usually think of functions of
multiple arguments?
Email Gateway (Aug 18 2022 at 18:39):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
This discussion reminds me of this thesis:
http://people.pwf.cam.ac.uk/mg262/GanesalingamMdis.pdf
I've only read fragments of it, but particularly relevant to what
started this whole discussion is the observation on page 189 that the
standard set theory definition of functions doesn't reflect how
mathematicians actually think of functions. In particular, according to
that definition, functions don't have unique codomains. (The footnote
about this observation being novel indicates that the author was unaware
of page 19 of Topoi: http://tinyurl.com/7qx72ou . In the interests of
full disclosure, the author of Topoi is Rob Goldblatt, who is my current
supervisor.)
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 18:39):From: James Frank <james.isa@gmx.com>
Thanks for the link.
The range/codomain part of function definition shows that much of math
is just logic games.
To prove that f is a function, you have to show that for every element
in the domain, there exists an element in the codomain that it's mapped
to. But the best you might can do is show that it maps to an element in
some interval. So someone, somewhere back in history, conveniently
decided to loosen up the definition of function to allow that.
Otherwise, a tighter definition of function becomes a big show stopper.
Begin reasonably pragmatic, I'd say all these logic games are useless
other than the fact that it recently occurred to me that using the Axiom
of Choice is not just a useless logic game. If you can know two sets
aren't equal, and the Axiom of Choice can give you that, then that's useful.
As to how this applies to me, it's not my fault. I'm a product of a
centuries old university system that has programmed me to have certain
expectations, and want certain things.
--James
Email Gateway (Aug 18 2022 at 18:40):From: James Frank <james.isa@gmx.com>
Ramana,
Thanks again for the help. I'll answer your last question first, and
then go long-winded on you.
_Q_: Representations 2 and 3 are closely related. Indeed, you can write
a (higher-order) function to transform a curried function into an
uncurried function (and vice versa). Are any of these close to how you
usually think of functions of multiple arguments?
Yes, #3 pretty much represents multi-variable calculus. It's all about
having a function f:R^n --> R^m. N-tuples. It's all about n-tuples.
As to currying, in the Haskell books, it was quickly pointed out that
though curried functions were primarily being used, as you say, which
they said, going back and forth between curried functions and uncurried
functions is not a problem. All these details about curried functions
will help me if curried functions become a part of what I'm doing.
However, the reason that we're having to talk about multi-variable
functions, in relation to function composition, is not because of how
function composition is implemented with sets, but how it's implemented
without sets.
The definition of sets function composition doesn't make it a function
which takes multiple arguments. If the domain is a collection of
n-tuples, then we have a multi-variable function. If not... I always get
paranoid when making technical claims, even if they're basic.
I'll stop here. All I have to do flip a mental switch. Initially, I make
it my goal to prove every theorem in Rudin just like he does. If I flip
a switch, then I decide it's good to implement them with proofs founded
on curried functions.
But I still have questions, which you don't need to answer. Are curried
functions merely part of implementation, or can they be abstracted out?
Where am I going to find the definition of function? I see that function
is already being used in Fun.thy. I see that Groups.thy is two levels up
from HOL.thy, and functions are used in groups. My guess is that I'm
going to find function at the compiler level.
Thanks,
James
Email Gateway (Aug 18 2022 at 18:40):From: Ramana Kumar <rk436@cam.ac.uk>
On Mon, Nov 7, 2011 at 6:08 PM, James Frank <james.isa@gmx.com> wrote:
Ramana,
Yes, #3 pretty much represents multi-variable calculus. It's all about
having a function f:R^n --> R^m. N-tuples. It's all about n-tuples.As to currying, in the Haskell books, it was quickly pointed out that though
curried functions were primarily being used, as you say, which they said,
going back and forth between curried functions and uncurried functions is
not a problem. All these details about curried functions will help me if
curried functions become a part of what I'm doing.
Good. I'm glad they were both familiar already.
But I still have questions, which you don't need to answer. Are curried
functions merely part of implementation, or can they be abstracted out?
I'm not sure what you mean. You said "or" between two things that
would go together. I think the answer is "no".
Where am I going to find the definition of function? I see that function is
already being used in Fun.thy. I see that Groups.thy is two levels up from
HOL.thy, and functions are used in groups. My guess is that I'm going to
find function at the compiler level.
Functions are fundamental to HOL, so you're right if you're calling
that the "compiler level". (But you don't have to go to the ML
compiler level!) The function type operator (the "=>" we were using
before) is primitive, that is, not created by type definition. In the
usual model of HOL in set theory, it constructs function spaces.
Email Gateway (Aug 18 2022 at 18:40):From: James Frank <james.isa@gmx.com>
Ramana,
Makes sense, I guess. And even in src/ZF/ZF.thy I see that primitive.
It's all functional programming. That's my revelation of yesterday.
Anything that gives me recursion is probably going to be functional
programming.
My requirements have changed. All I want is the easiest possible way to
learn a tool that allows me to do some logic and have the appearance of
sets. If there's a problem, it's false illusions.
Thanks,
James
Email Gateway (Aug 18 2022 at 18:41):From: James Frank <james.isa@gmx.com>
I'll ask the easy question first. In my inbox, there's
isabelle-users@cl.cam.ac.uk and cl-isabelle-users@lists.cam.ac.uk . Does
it make any difference which address I use to send in a question? If it
doesn't, you don't need to answer that question.
I've tried not to ask different forms of my next question. That's
because after studying enough type theory, lambda calculus, functional
programming, and files from ~~/src/HOL, I'll figure out most of the
answers. But that could be up to a years worth of work, and I'm trying
to get a feel for where this road is going, and whether I may need to
travel the road less traveled.
My question, stated very general, is this: "Can I take a file such as
~~/src/HOL/Fun.thy, rephrase the definitions in the language of standard
math definitions and theorems, with a few changes to accommodate types,
and have these standard definitions/theorems be describing the same
objects as the Isabelle definitions and lemma?" I'm not talking about
starting with a different logical framework or set of axioms, and ending
up at the same place.
Below I ask related questions which are probably more straight forward
to answer, and, if answered, might answer the question just posed.
To get more specific, I'll ask some questions about "definition comp" in
Fun.thy, which is the definition of function composition.
First, here are some related goals to set the context, for why I'm
thinking about this now:
1) I want to cater to mathematicians who are doing traditional
mathematics. Therefore, the language of my definitions and theorems
needs to be reasonably familiar to them. I'd like to start rephrasing
Isabelle defs and thms now.
2) I want to build on, and learn from, what others have done. Therefore,
my first choice is HOL rather than ZF, since the library is larger, even
though HOL is not as "traditional".
Here's the definition of comp from Fun.thy:
definition comp :: "('b => 'c) => ('a => 'b) => 'a => 'c" (infixl
"o" 55) where
"f o g = (\<lambda>x. f (g x))"
Studying Haskell is what led me to Isabelle, and I studied just enough
functional programming to know that comp is a function that takes type
"('b => 'c)" and returns type (('a => 'b) => 'a => 'c)). I guess that's
right, although I ask below about (\<lambda>x. f (g x)), and about its
domain and range.
Functions have domains and ranges. You won't be surprised here, but
never once have I seen "function composition" be defined with the domain
being a set of functions, and the range being a set of functions whose
elements are functions, which take functions, and return functions.
Here's what I want out of "definition comp", using more standard math
language:
DEFINITION 1.1.1 (comp). Let g:'a-->'b and f:'b-->'c. Then (f o
g):'a-->'b, where (f o g)(x) = f(g(x)).
Notice that I tweak the definition to use types rather than sets. I was
also tempted to stick "(f o g) = (%x. f(g x))" in there, not that I know
much more than what it symbolizes. The details and groundwork could be
worked out if it's basically the same thing as "comp".
A pertinent point here is that with a definition such as DEFINITION
1.1.1, I'm not making many demands on someone. They might be willing to
go with it even with only an intuitive understanding of types and lambda
calculus. However, it's important to me that something like DEFINITION
1.1.1 and "comp" be the same thing. Not be like, "think of them as the
same", but "are the same".
Okay, what I really want is something like this:
(f o g) = {(a,c) in AxC | ThereExists b in B, such that (a,b) is in
g and (b,c) is in f}.
You can tell me different, but I assume I'm correct in saying that
"comp" is not this set, and can't be this set, though with some work,
some form of equivalence could be shown. Again, I guess that's right.
Somewhere in this question is me trying to figure out how different
"comp" is from a standard definition of composition. Is "comp" close
enough to a standard definition to try and phrase it using standard
language, or it's "functional programming, type theory, and lambda
calculus", and I should just accept it for what it is. Regardless, it is
what it is, and I want to describe it as what it is, but describe it
using language other than Isabelle code.
POINT 1: In a standard definition of function composition, there are
typically three functions, "f", "g", and "f o g".
POINT2: In "comp", there are four functions, "f", "g", "(\<lambda>x. f
(g x))", and the function of type
"('b => 'c) => ('a => 'b) => 'a => 'c".
What I've said above might could be summarized with this question:
What is this thing, this function "('b => 'c) => ('a => 'b) =>
'a => 'c"?
If I have to incorporate that into my traditional-style definition, then
it's no longer traditional-style. If I have to do that, then I'm doing
something different.
If it's necessary details, and a way of specifying "g:'a-->'b,
f:'b-->'c, and (f o g):'a-->'b", and I can easily formalize the
connection prior to my function composition definition, then the
situation is salvageable.
Anyway, feel free to comment or not.
Thanks,
James
Email Gateway (Aug 18 2022 at 18:41):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
On 08/11/11 05:00, James Frank wrote:
To prove that f is a function, you have to show that for every element
in the domain, there exists an element in the codomain that it's mapped
to. But the best you might can do is show that it maps to an element in
some interval.
What? Why?
So someone, somewhere back in history, conveniently
decided to loosen up the definition of function to allow that.
To allow what? I'm not convinced that anyone deliberately decided that
the definition of functions shouldn't correspond with how mathematicians
actually think about them. I think it's just a long-standing imprecision.
Otherwise, a tighter definition of function becomes a big show stopper.
Why? Can you give an example?
--James
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 18:42):From: Ramana Kumar <rk436@cam.ac.uk>
There are many ways to go about answering your question, and I'm sure
other people on the list will make better attempts than me. But I hope
multiple answers will help you, at least for different perspectives.
The main thing I want to say is that I think the situation is
salvageable: functional programming, (simple) type theory, and lambda
calculus are not so far removed from traditional mathematics.
You may be interested also in looking at Higher Order Set Theory. But
for now let's stick with HOL.
I'll make a few specific comments below, under the relevant bits of
your message.
On Thu, Nov 3, 2011 at 6:45 PM, James Frank <james.isa@gmx.com> wrote:
My question, stated very general, is this: "Can I take a file such as
~~/src/HOL/Fun.thy, rephrase the definitions in the language of standard
math definitions and theorems, with a few changes to accommodate types, and
have these standard definitions/theorems be describing the same objects as
the Isabelle definitions and lemma?" I'm not talking about starting with a
different logical framework or set of axioms, and ending up at the same
place.
I think yes.
Functions have domains and ranges. You won't be surprised here, but never
once have I seen "function composition" be defined with the domain being a
set of functions, and the range being a set of functions whose elements are
functions, which take functions, and return functions.
Have you seen it being defined as a function before? If so, what was
its domain and range?
(I also want to ask: how would you usually think of an ordinary
function that takes two arguments? This line would continue into a
discussion about currying, but I'll leave it out for now.)
Here's what I want out of "definition comp", using more standard math
language:DEFINITION 1.1.1 (comp). Let g:'a-->'b and f:'b-->'c. Then (f o g):'a-->'b,
where (f o g)(x) = f(g(x)).
This looks like a definition of composition as an "operator", rather
than a function. From a "first-order" perspective, since functions are
on a higher level than the values they take and receive, we need a
separate concept for things like comp that operate on functions
themselves. Notice that Definition 1.1.1 doesn't ever say that "o"
itself is taking arguments and returning a value, rather, it specifies
what the function "f o g" (which is really a function and not an
operator) does by saying what it does on arguments.
When you switch to the "higher-order" perspective, these distinctions
all disappear. Functions are values too, and operators that
take/receive functions are also just functions. So the function
composition operator is itself a function.
Okay, what I really want is something like this:
(f o g) = {(a,c) in AxC | ThereExists b in B, such that (a,b) is in g and
(b,c) is in f}.You can tell me different, but I assume I'm correct in saying that "comp" is
not this set, and can't be this set, though with some work, some form of
equivalence could be shown. Again, I guess that's right.
It could be that set in a model of HOL, but the sets in the model
wouldn't be the same as the sets encoded in Set.thy for example. To
avoid confusion, perhaps I should just say "you're right, comp is not
that set, but it is in some sense equivalent."
POINT 1: In a standard definition of function composition, there are
typically three functions, "f", "g", and "f o g".POINT2: In "comp", there are four functions, "f", "g", "(\<lambda>x. f (g
x))", and the function of type
"('b => 'c) => ('a => 'b) => 'a => 'c".
The fourth function in "comp" is function composition itself (denoted by "o").
Email Gateway (Aug 18 2022 at 18:42):From: James Frank <james.isa@gmx.com>
Tim,
Thanks for the question, primarily so I can leave in a civilized manner
and say something positive. By asking my question, I've made about 3
transitions.
It was functional programming, then proof assistants, and now it's all
the same. In messing around with Isabelle for about a month, it raised
my awareness so that I could see that Coq is a functional programming
language. Coq provides me with a book which will teach me functional
programming and the proof assistant software at the same time. Isabelle
starts at the intermediate level in regards to functional programming.
That's too high for me.
Everyone here has been very helpful, accessible, and professional. I'm
not a professional, and I don't act like one.
Now to your questions.
SHORT ANSWER: Let f(x)=sin(x).
REFERENCE: http://www.angelo.edu/faculty/cdiminni/ . The area code is
actually 325, not 915.
YOU ASK: What? Why?
Because the definition requires it.
Let f be a subset of AxB. Then f is a function if
1) for every x in A, their exists some y in B such that (x,y) is in f, and
2) if (x,y1) is in f, and (x,y2) is in f, then y1=y2.
We call A the domain of f, and we call B the codomain of f. The range of
f is that subset of B... It's getting obnoxious at this point. The range
is the actual values that the x's are mapped to.
YOU ASK AND SAY: To allow what? I'm not convinced that anyone
deliberately decided that the definition of functions shouldn't
correspond with how mathematicians actually think about them. I think
it's just a long-standing imprecision.
I'm not a historian. I was speculating on the reasons. It doesn't make
sense to continue to have such a loose definition of function unless
there's an advantage. EXAMPLE: Definition of limit. Newton and Liebniz
started limit (or used it). Weierstrass tightened it up. Everyone
accepted the tighter epsilon-delta definition.
WE ARGUE:
Email Gateway (Aug 18 2022 at 18:42):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
On 11/11/11 06:28, James Frank wrote:
SHORT ANSWER: Let f(x)=sin(x).
This could define several different functions. For example, it could
define a function from the complex numbers to the complex numbers; it
could define a function from the real numbers to the real numbers; or,
it could define a function from the real numbers to [-1,1]. The point
is that according to the standard definition of functions, the last two
are identical.
YOU ASK: What? Why?
Because the definition requires it.
Let f be a subset of AxB. Then f is a function if
1) for every x in A, their exists some y in B such that (x,y) is in f, and
2) if (x,y1) is in f, and (x,y2) is in f, then y1=y2.We call A the domain of f, and we call B the codomain of f.
But "the codomain" isn't well defined. I think the example from Topoi
illustrates my point quite well. What is the identity function on the
natural numbers? According to the traditional definition, the answer is
{(0,0), (1,1), (2,2), ...}.
What is the injection function from the natural numbers to the integers?
{(0,0), (1,1), (2,2), ...}.
The traditional definition requires that an identity function on a set A
is exactly the same function as every injection function from A to any
superset of A. I don't believe that this is how mathematicians actually
treat identity and injection functions.
And the crucial thing is this: If I ask "What is the codomain of
{(0,0), (1,1), (2,2), ...}?",
the answer has to be that the codomain isn't uniquely defined, but must
be some superset of the natural numbers.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 18:46):From: Lawrence Paulson <lp15@cam.ac.uk>
There is a sense in which your question is not entirely meaningful, because you're asking whether rigorous but informal mathematics is adequately captured by a particular formalisation, and such issues are ultimately subjective. However, traditional mathematics is often assumed to be based on set theory, and higher-order logic has very straightforward models in set theory. In particular, if you look at the function f o g, then you get exactly the same set of ordered pairs by either route, assuming you're in the mood to interpret a function as a set of ordered pairs. The situation with higher-order logic is very different from that presented by various constructive type theories you may have seen, where you typically cannot regard a function as a set of pairs.
Some of the other points that you mention relate to basic lambda-calculus. There is no need to study the lambda calculus in its full glory, as it is quite irrelevant to higher-order logic. Lambda-notation merely expresses the notion of a function, something that is curiously lacking in standard mathematical practice. The type of the composition operator is a well-known device, known as currying, for expressing functions that take multiple arguments. Again, traditional mathematics is quite careless in such situations. You remark that functions have domains and ranges, but typically the function composition operator is not written in such terms at all, and is allowed to apply to any compatible pairs of functions whatever. In the language of set theory, it is a class function.
Anything that you can define in higher-order logic is not merely explicable in traditional mathematical terms, but it is easily so. But there are plenty of things you can write in mathematics that are impossible to formalise in higher-order logic. This is because mathematics is essentially open-ended.
Larry Paulson
Last updated: Apr 20 2024 at 08:16 UTC