From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1352 Path: news.gmane.org!not-for-mail From: Dusko Pavlovic Newsgroups: gmane.science.mathematics.categories Subject: Re: Real midpoints Date: Mon, 17 Jan 2000 20:07:28 -0800 Message-ID: <3883E700.797D12A9@kestrel.edu> References: <200001170123.UAA13135@liberty.math.lsa.umich.edu> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241017769 30842 80.91.229.2 (29 Apr 2009 15:09:29 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:09:29 +0000 (UTC) Cc: Categories List To: Peter Selinger Original-X-From: rrosebru@mta.ca Tue Jan 18 10:24:36 2000 -0400 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA04610 for categories-list; Tue, 18 Jan 2000 09:02:30 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: Mozilla 4.5 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 13 Xref: news.gmane.org gmane.science.mathematics.categories:1352 Archived-At: > My point is that the definition of g is neither recursive nor > co-recursive. The definition of g is merely expressed as a fixpoint > equation, and Peter has set up things so that there is indeed a unique > solution to this equation. However, the reason the fixpoint is unique > is because the "h" part is contracting, and not because the equation > is co-recursive. what exactly do you mean by corecursive? (it's guarded, and guarded equations do have unique fixpoints.) -- dusko