Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.math
Subject: For a 100th Time Fuck Stackexchange (Re: Honoring Raymond Smullyan)
Date: Wed, 8 Jan 2025 10:55:15 +0100
Message-ID: <vlli22$2043g$2@solani.org>
References: <vlkg09$1vh4j$2@solani.org>
 <r7md26ferwv7.mm1ked0log2e.dlg@40tude.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 8 Jan 2025 09:55:14 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2101360"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:ah36z30RnQQGORW749sdmaYh5LI=
In-Reply-To: <r7md26ferwv7.mm1ked0log2e.dlg@40tude.net>
X-User-ID: eJwFwQcBwDAMAzBKeXYXOMspfwiV4FT2CYKBixtmNdOGACnhlpmKj9bU3B2v9c1Dz/y1R7aEoRCtOS3gAyqHFHQ=
Bytes: 3223
Lines: 69

I upvoted this question:

Curry-Howard Correspondence using Smullyan's bird forests
https://math.stackexchange.com/q/1927260/1482376

And made an answer.

Guess what happened, it took a few hours
and my answer that I posted here was down
voted, and the question was also down voted.

Looking at it again after a 8 hours
the question was again down voted. Thats
why I don't use stackexchange anymore, only ChatGPT.

You can ask ChatGPT with no problem:

https://chatgpt.com/share/677e4ab2-8808-8013-b1ce-740889795507

You're absolutely right—there are no mockingbirds
in Simply Typed Lambda Calculus because mockingbirds,
as described in To Mock a Mockingbird, mimic other
birds. Mimicry introduces self-referential behavior,
which is akin to the untyped lambda calculus where
recursion and self-reference are allowed.

In Simply Typed Lambda Calculus, the forest is stricter:

Every bird has a fixed type and follows specific
rules about whom it can sing to and what kind of
song it can produce. There are no "self-referential" birds
because they would break the typing rules. In type-
theory terms, the absence of recursion makes the system
well-behaved and strongly normalizing (every song ends eventually).

If we wanted mockingbirds in this framework, we’d
need to move to a typed calculus that supports
recursive types or explicit fixed-point combinators
(like Y in untyped lambda calculus). Would you like
a bird-forest analogy for recursion or fixed-point
combinators as well?

Tom Bola schrieb:
> Am 08.01.2025 01:14:02 Mild Shock schrieb:
> 
>> Hi,
>>
>> Now you can listen to Bird songs for a minute:
>>
>> 2016 Dana Scott gave a talk honoring Raymond Smullyan
>> https://www.youtube.com/watch?v=omz6SbUpFQ8
> 
> That is really a very great analysis!
> 
>> A little quiz:
>>
>> Q: And also on the Curry-Howard Isomorphism. Is
>> there a nice way to put it in bird-forest form like To
>> Mock a Mocking Bird. This book made everything so
>> simple and intuitive for me.
>>
>> A: Hardly, because xx has no simple type.
>>
>> Right?
> 
> I guess so...
> 
> A great many thanks for posting all that!
>