| an explanation of Curry's paradoxical Y combinator, which in the
| lambda_calculus defines recursive functions.
Thanks, that's an interesting discussion!
John, I'd be thrilled if you read it, and you'd be the first. Sorry
for leaving on the to- & cc-lists. Partly I wrote it because I was so
dissatisfied with Matthias Felleisen's explanation of the Y combinator
in his book The Little Schemer. BTW I only learned how to code in
Scheme after reading Felleisen's free book HtDP.
Thanks for the responses, which I'll study, and I'm glad you fixed the
camlp5 biz. One remark about sets and geometry axioms:
Seems we should be able to define a Tarski model to be a triple
(S, Between, Equiv) where
S is a set (of our points),
Between is a subset of the Cartesian product C^4, and
Equiv is a subset of the Cartesian product C^3,
where the 7 axioms involving Between and Equiv hold.
I think in HOL you define Cartesian products using lambda, which sorta
makes sense, because an element of C^4 is a function
{1,2,3,4} -> C.
That's a switch for me, because in Scheme you're taught not to do
this, because the lambda doesn't get evaluated soon enough.
Does this sound like a good idea? And the only improvement would be
to able to make a global declaration that we're using the Tarski model
(S, Between, Equiv) over the next 38 theorems & proofs.
You keep referring to Phil's work, and maybe he's solved all these
problems. Is his code available for studying (and borrowing)?
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
