From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 85AE6BB9C for ; Fri, 6 Jan 2006 14:12:15 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k06DCEGK025888 for ; Fri, 6 Jan 2006 14:12:15 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id OAA06163 for ; Fri, 6 Jan 2006 14:12:14 +0100 (MET) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k06DCCjp025878 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Fri, 6 Jan 2006 14:12:14 +0100 Received: from localhost ([127.0.0.1] ident=andrej) by haka.fmf.uni-lj.si with esmtp (Exim 4.50) id 1EurO8-0005Gk-0q; Fri, 06 Jan 2006 14:12:12 +0100 Message-ID: <43BE6CAB.2030503@andrej.com> Date: Fri, 06 Jan 2006 14:12:11 +0100 From: Andrej Bauer User-Agent: Debian Thunderbird 1.0.2 (X11/20050331) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Alessandro Baretta , caml-list@inria.fr Subject: Re: [Caml-list] Coinductive semantics References: <43BD6418.4090407@barettadeit.com> In-Reply-To: <43BD6418.4090407@barettadeit.com> Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 127.0.0.1 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com X-SA-Exim-Scanned: No (on haka.fmf.uni-lj.si); SAEximRunCond expanded to false X-Miltered: at concorde with ID 43BE6CAE.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43BE6CAC.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 coinductive:01 semantics:01 baretta:01 algebra:01 non-trivial:01 algebra:01 subset:01 arity:01 binary:01 binary:01 non-trivial:01 trivial:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Alessandro Baretta wrote: > Is there anyone around who can help? Induction is about initial algebras. It says that an initial algebra does not have any non-trivial SUB-algebras. General induction principle for the initial algebra A with operations f_1, ..., f_n (some of which may be 0-ary operations, i.e., constants) goes as follows: INDUCTION PRINCIPLE: Suppose S is a subset of A which is closed under operations f_i, meaning that if x_1, ..., x_{k_i} are in S then also f_i(x_1, ..., x_{k_i}) is in S (here k is the arity of operation f_i). Then S = A. If we apply this to the case when we have one constant f_0=Empty and one binary operation f_1=Tree, we get as A all finite binary trees and the induction principle: INDUCTION PRINCIPLE FOR FINITE BINARY TREES: Suppose S is a set of finite binary trees such that the empty tree is in S, and whenever x and y are in S then also tree Tree(x,y) is in S. Then S is the set of all finite binary trees. Now coinduction is about final coalgebras. It says that a final coalgebra does not have any non-trivial QUOTIENT coaglebras. This is usually expressed as follows: if F is the final coalgebra for operations f_1, ..., f_n, and E is an equivalence relation on F which respects the operations, then E is the identity relation (because if it were not, we could form a nontrivial quotient coaglebra F/E). The actual coinduction principle may be stated for an arbitrary relation R (think of E as the equivalence relation generated by R): COINDUCTION PRINCIPLE: Suppose R is a relation on the final coalgebra F which respects the operations, i.e., if x_1 R y_1, ...., x_{k_i} R y_{k_i} then f_i(x_1, ..., x_{k_i}) R f_i(y_1, ..., y_{k_i}) for all x's, y's and f_i's. Then R(x,y) implies x = y. An R satisfying the above condition generates the trivial equivalence relation (equality) and so the quotient F/R is just F. We take again as example the final coalgebra F with one constant f_0=Empty and one binary operation f_1=Tree. This is the set of finite and infinite binary trees. COINDUCTION FOR (FINITE AND INFINITE) BINARY TREES: Suppose R is a relation on trees such that: (1) Empty R Empty (2) if x R y and x' R y' then Tree(x,y) R Tree(x',y'). Then x R y implies x = y. It takes some practice to get used to coinduction and to figure out how to prove properties of final coalgebras with it. If this was too terse, let me know (and tell me which bits to expand upon). Andrej