Dear Bill, I agree (mostly) with your points. What you describe is a T-coalgebra (in terms of computer science), which is given by a functor (monad) T. You look at structures like maps a : V --> TV, where V is a data type and T the monad, a is an algebra (map). Coalgebras come with the principle of coinduction [proof principle, works for non-well founded sets] (while T-algebras (also in the sense of computer science, which are maps of a type b : TV ---> V) come with recursion). Given that you have a final coalgebra you can prove some things. There is a vast literature about this in computer science, look for example at J.J.M.M. Rutten's paper "Universal coalgebra: a theory of systems", Theor. Comp. Sci. 249 (2000) 3-80.
I do not so much agree with what you said about Heyting algebras. Domain (and type) theory has some devices to deal with infinite calculations, its not so much about Heyting (internal topos logic) but just adding a new bottom to the type which says computation does not return anything (infinite) (in case of ?finite for an infinite stream where no other information is available). The logic comes into play, when you really want to specify what kind of programs (functions) you want to run (they need to be continuous, so you need to specify a topology, which in turn comes from a DCPO or such) and the choice of topology may propel you deep into constructive (and/or topos valid) logic [not that there are many `constructiv mathematics' out there, ...]. Types tend to be localic. So, yes, boolean logic and constructive mathematics does not go well together. Haskell has a `maybe' monad. In terms of Ralf's question, a stream s if asked ?finite may return `yes|maybe|no' and only two of this cases provide actual information. (Not that here no(yes) is not no and not(no) is not yes ...) Does AXIOM have monads (like Haskell)? Sorry not much time to investigate myself. Such things can be implemented very efficiently and in an encapsulated way by using monads (in Haskell). Hence I would not see that lazyList would help, as you use streams also for really large but finite lists when evaluating it (there is a command to turn a stream into a list, forgot its name) as it would not fit into memory.... Cheers BF. tl;tr [BTW: My colleague Martin Escardo writes Haskell (and Agda) programs which search transfinite sets using such methods, really stunning..., you might want to check out his webpage : http://www.cs.bham.ac.uk/~mhe/ ;-)) ] -- % PD Dr Bertfried Fauser % Research Fellow, School of Computer Science, Univ. of Birmingham % Honorary Associate, University of Tasmania % Privat Docent: University of Konstanz, Physics Dept <http://www.uni-konstanz.de> % contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/ % Phone : +44-121-41-42795 -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to fricas-devel@googlegroups.com. To unsubscribe from this group, send email to fricas-devel+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
