From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp12.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id GIVKHVzvwmINbAAAbAwnHQ (envelope-from ) for ; Mon, 04 Jul 2022 15:47:08 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp12.migadu.com with LMTPS id UOkcHVzvwmIbywAAauVa8A (envelope-from ) for ; Mon, 04 Jul 2022 15:47:08 +0200 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id EB950A06 for ; Mon, 4 Jul 2022 15:47:07 +0200 (CEST) Received: from localhost ([::1]:39674 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1o8MPq-0002hD-1N for larch@yhetil.org; Mon, 04 Jul 2022 09:47:07 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:35524) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1o8LyT-0002pL-TC for emacs-orgmode@gnu.org; Mon, 04 Jul 2022 09:18:59 -0400 Received: from mail-out02.uio.no ([2001:700:100:8210::71]:57913) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1o8LyI-0002Ms-Ka for emacs-orgmode@gnu.org; Mon, 04 Jul 2022 09:18:40 -0400 Received: from mail-mx10.uio.no ([129.240.10.27]) by mail-out02.uio.no with esmtps (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from ) id 1o8LyE-00AhnN-6n for emacs-orgmode@gnu.org; Mon, 04 Jul 2022 15:18:34 +0200 Received: from [84.209.16.135] (helo=fedora.shmi.ifi.uio.no) by mail-mx10.uio.no with esmtpsa (TLS1.2:ECDHE-RSA-AES256-GCM-SHA384:256) user msteffen (Exim 4.94.2) (envelope-from ) id 1o8LyD-0005M0-Hx; Mon, 04 Jul 2022 15:18:34 +0200 From: Martin Steffen To: emacs-orgmode@gnu.org Subject: Re: [more absurd] Organization: IFI UiO Norway References: <87iloeatbo.fsf@mat.ucm.es> <87bku6arzq.fsf@mat.ucm.es> <875ykeaqrh.fsf@mat.ucm.es> <87zghpa2f0.fsf@mat.ucm.es> <86o7y5ide4.fsf@login.ifi.uio.no> Date: Mon, 04 Jul 2022 15:18:31 +0200 In-Reply-To: (tomas@tuxteam.de's message of "Mon, 4 Jul 2022 14:12:23 +0200") Message-ID: <867d4thv88.fsf@login.ifi.uio.no> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-UiO-SPF-Received: Received-SPF: neutral (mail-mx10.uio.no: 84.209.16.135 is neither permitted nor denied by domain of ifi.uio.no) client-ip=84.209.16.135; envelope-from=msteffen@ifi.uio.no; helo=fedora.shmi.ifi.uio.no; X-UiO-Spam-info: not spam, SpamAssassin (score=-5.0, required=5.0, autolearn=disabled, T_SCC_BODY_TEXT_LINE=-0.01, UIO_MAIL_IS_INTERNAL=-5) X-UiO-Scanned: 610C4AF78E97862325E4B91AC9AD80720F648846 X-UiOonly: 8A1BE50D217B32D284C08446418ECE613F384E1B Received-SPF: pass client-ip=2001:700:100:8210::71; envelope-from=msteffen@ifi.uio.no; helo=mail-out02.uio.no X-Spam_score_int: -18 X-Spam_score: -1.9 X-Spam_bar: - X-Spam_report: (-1.9 / 5.0 requ) BAYES_00=-1.9, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: emacs-orgmode@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: "General discussions about Org-mode." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-orgmode-bounces+larch=yhetil.org@gnu.org Sender: "Emacs-orgmode" X-Migadu-Flow: FLOW_IN X-Migadu-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1656942428; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post; bh=m7buwTlwaM9cw+V23r3LzDPxCkOKkXj/83lS6uJ6J/U=; b=KiFPx9VNex7hTTAoG2PC2t/fApAFULXUo7muQCoX0eG/bD3HKfjNUJUtPA9MYYA9KFGX/d wZ1Algi17ErQP1VgoVV8c2rJ9KoNVllfF/h8lQ/vOS911M4mZpV+ptnk510Nd0WKQYRSH3 PtSHuIaewctdmcd5b/PuAReFrl6P6HDp6B/CXtLQlO+2OGXTKQMCHDME66kQV1Z4hbPSG/ 2tNr0UQgeeifZNn2gSllXbjVvT9gM5ie5jZZk0Lfbm58TRXDX/s59SJiUxoHXj+x7LqgRG YzbOErw2mHWq4KE7gSPGiedTtPsVt8Bjk+zGdu3ltBR6mchbQOSzKtN+HgNW/A== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1656942428; a=rsa-sha256; cv=none; b=q40EtMxdwg+a2QSiv0nFbu0lnCkS4srn0xiAHXs77C+uspSjuV5SyWxF3gY/EnbjDNPlNQ ODBQ36iFiEbeSfT99yxiJyfVl96oGyrG8AqzIIPafH2KQyLnqNJxcd6J+p7SSMBt/il3wG 1tr2YSG8hd9q8WE3C5YAp6lWY6upJmwXgvoJrFdK6kc+RSMp1jzT521FbRpaH9CoZgWef4 EdDFj3a3/GpaE/kkkwcPP5G7FTtss5kbOvCYBsDMCtNMI7AvTqQhQkOcj5MT8Zj3KVR/wW 6roPteyxAkoAPrE62F/7hF8O24c6VbPD3LIIfTKv4j2KrRaQYTS2WVXVTGwakA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; dmarc=none; spf=pass (aspmx1.migadu.com: domain of "emacs-orgmode-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="emacs-orgmode-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: -2.75 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=none; spf=pass (aspmx1.migadu.com: domain of "emacs-orgmode-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="emacs-orgmode-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: EB950A06 X-Spam-Score: -2.75 X-Migadu-Scanner: scn1.migadu.com X-TUID: itQwy8oqMw7L >>>>> writes: > About the cultural thing... you seem to be a zero-counter (as I I guess I am, by maybe have not been a zero-counter from the start, but a 1-counter. I vaguely remember to have learnt (at school? beginning at university?) that ``THE natural numbers'' (the ones Kronecker claimed to have been created by God) start with $1$. There are referred to by $\mathbb{N}$, and then there's also some versions, written $\mathbb{N}_0$ (THE natural numbers ``extended'' by 0), they can be handy too, sometimes. >From a constructivistic point of view (and as a computer scientist, one is obliged to have a constructivist view), for me 0 belongs to the most natural way of defining natural numbers. The fact that some theorems or facts are stated better this way or the other is minor (as long as it's not that the vast majority of math on Nats gets simpler without 0 (or with 0). One would also not work with Nats starting at two like Nat ={2, 3,4,...}, for the extravagant advantage to avoid stating clumsily a special-case condition ``a prime number is a natural number larger or equal 2 and only divisible by 1 or itself'' (if one thinks 1 and 0 are better not included in the prime numbers, as most would do). Constructing the nats from first principles seems to me a Nat is either 0, or the successor of a nat (succ n). Also for lists (and in complete analogy): Lists are either empty () or built from cons-ing an element to a list. An analogous construction would of course also work using 1 as base case resp. a one-element list as basic constructor. But it ``feels'' less natural for me in the meantime. [talking about programming and data structures: while I think from a practical (and aesthetic) point of view, lists should include the empty list, and not start with lists of length 1 (likewise that functions should be allowed to have a 0-length input parameter list), I found it interesteding that _internally_, lists and similar data structures are often usefully implemented with some ``sentinel'' node, i.e., the empty lists is represented by some ``dummy cell'' in memory (not by ``nothing''), and a list of length n has additionally one such dummy cell at the end, say, to make walking through the list, resp. checking for the end more smooth and uniform, sometimes.] > am, too): there, too, I think that "our" position isn't in any way > "better" -- some theorems look better this way, some that way; > some inductions are easier to start at 1, some at 0. > Cheers -- t