|From: Lennart Augustsson <[EMAIL PROTECTED]>
|To: Jan Brosius <[EMAIL PROTECTED]>
|Cc: Frank Atanassow <[EMAIL PROTECTED]>; <[EMAIL PROTECTED]>
|Sent: Friday, May 19, 2000 12:07 PM
|Subject: Re: more detailed explanation about forall in Haskell
> Jan Brosius wrote:
>
> > > "x" in the domain of your model, and that that element, at least,
> > satisfies
> >
> > x is a variable ; no domain ; no model
>
> You must have some assumed convention that makes x a variable.
That's true . To be complete in Bourbaki's formal logic they don't speak in
the beginning about
a variable but they define a substitution mechanism for ONLY small latin
letters ,denoted
( T | u) S
which means replace in S , being just consecutive string of symbols, every
occurence of the letter u
by T , which itself is also a consecutive string of symbols , I think this
corresponds to
(T | u) S == (lambda u . S) T
(as far as I know lambda- calculus)
Of course they begin with a set of allowable symbols.
Later when they talk about a mathematical theory they introduce the
"metha-mathematical " notion of variable
in the following sense a letter t is a variable of the theory if this
letter does not occur explicitly
in one of the axioms of the theory.
Another way to introduce a variable would be to use a special letter say x
and to say, that a variable
is an x subscripted by an integer number , this would mean that only x0 ,
x1 , x2 , ... ,x10 , etc. ..
are variables.
But this is not the place to explain in full detail Bourbaki's approach of
formal logic . I thought there is a common
consensus in logic about a variable.
Allow me to come back to to some meaning of variable expressed by someone
else in a previous email.
A person said something like this " alpha(x) means that alpha(x) is true
for some x " (where alpha(x) denotes
a formula containing a variable x .)
Now if one looks carefully this above sentence means formally
[exists x. alpha(x) is true] which is a FALSE assertion. To be honest he
didn't wrote the above english phrase
not like this , but he represented it by the implication
alpha(x) => [exists x . alpha(x)] which is a totally other thing . This
implication should more be read as
" if alpha(x) is true for some x then there exists an x such that alpha(x)
is true" Now as everybody can see
the above phrase looks a bit strange . It would have been better to replace
it by
(T | x) alpha(x) => [exists x . alpha(x)] where T is a TERM not
containing the letter x
which can be read " if alpha(x) is true for some x = T then there exists an
x such that alpha(x) is true " which
is perhaps an english phrase that makes more sense (I don't know) . Bourbaki
uses this implication ( (T | x) alpha(x) => [exists x . alpha(x)] where T
is a TERM not containing the letter x ) as an axiom scheme for his theory
with
quantifiers . Bourbaki makes a distinction about axioms and speaks about
explicit axioms and axiom schemes.
But the above remarks would have lead the discussion off the road and also
not everybody knows about
Bourbaki.
When I referred to variables and to the forall quantifier I implicitly
thought that there was a common consensus
about the use of variables and the forall quantifier. Now it doesn't bite
me if someone regards variables as ranging
over a domain . But I had to reply since one was insinuating that I don't
understand the difference
between free and bound variables , that is saying as much as : you don't
understand logic.
As Mark Jones has allready said this thread should end or come to a
conclusion. Unfortunately he said more than that . He said that the
discussion was all about the difference a -> a and forall a. a -> a . And
that's not
true . One only has to read the first 2 or 4 emails about this thread of
discussion.
On the other hand someone's remark and about the meaning Haskell gives to
these two types and I wonder since today if one means by a -> a a type
indication to be understood as a function having this type signature
means that the function is only defined for some a 's and by forall a.
a -> a a type indication to be understood
as a function that is really defined for ALL type's a .
The above is just a question . If my interpretation is right then one can
change a -> a by [exists a. a -> a]
But again my first email didn't talk about that , as every reader willing to
look in the archives would acknowledge.
Friendly
Jan Brosius
PS : by saying weird I didn't mean illigitimate I meant more something like
"it surprises me" where I am talking
as a mathematician trying to use Haskell , not knowing the type system that
is used nor the theory behind it , only
being surprised that in some cases forall cannot be understood anymore as
forall in formal logic.
E.g. it is a true fact that Bourbaki doesn't use forall before a type , and
I thought it is common consensus in
formal logic used in math that one doesn't use a forall for a term.
So I began to wonder if it was impossible to rephrase e.g. runST and
newSTRef by bounded forall's
using 2 additional predicates Free(x) and Variable(x) . My claim is still
the same that it is possible to rephrase
these functions in such a way that it can be understood also by
mathematicians.
I am well aware that the predicates (I would prefer to speak about
functional relations) Free ( ) and Variable( )
are NOT IMPLEMENTED yet , so up to now these predicates serve only the
purpose of an additional
documentation ; one cannot write programs with them in Haskell. But I think
they might be useful.
E.g. let's trying to say that instead of the function
pr2 :: (a, b) -> b
pr2 (x,y) = y
I wanted a slightly differing function
pr2' :: forall a. [forall b `notin Free(a) . (a,b) -> b]
pr2' (x,y) = y
With the above I filter out all arguments having a type of the form (a,
T(a)) ; i.e. pr2' is nothing else but the restriction of pr2 to some strict
smaller domain.
Sorry, for this long PS but perhaps this might close the discussion thread .
Unless someone could show me
that I am dead wrong .
Jan
> For the rest of us it might as well be a constant, because there is
> no way to tell if it is a variable or not.
>
> --
>
> -- Lennart
>
>
>
>
