tag:blogger.com,1999:blog-6839602.post3737889011034547610..comments2017-03-09T15:26:17.288-08:00Comments on Everyone Else is Crazy: Non-constructive Proofs and ProductivityJim Applehttp://www.blogger.com/profile/11080395413026172939noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-6839602.post-9016570127686338722007-03-08T07:14:00.000-08:002007-03-08T07:14:00.000-08:00In Coq you can define co-structurally recursive fu...In Coq you can define co-structurally recursive functions. Coq has a syntactic requirement of at least one additional constructor on the structurally co-recursive argument. <BR/><BR/>This restriction can be "stretched" by transforming programs with a measure function or relation that proves productivity, that can then be transformed into an auxiliary structurally co-recursive argument.<BR/><BR/>In coq you don't just label it as productive or terminating, you aren't even allowed to define it if it isn't one of those two!Jacobianhttps://www.blogger.com/profile/14899896537888421449noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-68756111826904669252007-01-21T06:35:00.000-08:002007-01-21T06:35:00.000-08:00Productivity of twins means that the stream is ele...Productivity of twins means that the stream is elementwise terminating, even though the spine does not terminate. So you can (in this case at least) define productivity in terms of termination.Robinhttps://www.blogger.com/profile/05420921538604886480noreply@blogger.com