For a 100th Time Fuck Stackexchange (Re: Honoring Raymond Smullyan)

Liste des GroupesRevenir à s math 
Sujet : For a 100th Time Fuck Stackexchange (Re: Honoring Raymond Smullyan)
De : janburse (at) *nospam* fastmail.fm (Mild Shock)
Groupes : sci.math
Date : 08. Jan 2025, 10:55:15
Autres entêtes
Message-ID : <vlli22$2043g$2@solani.org>
References : 1 2
User-Agent : Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.19
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!
 

Date Sujet#  Auteur
8 Jan 25 * Honoring Raymond Smullyan9Mild Shock
8 Jan 25 +* Re: Honoring Raymond Smullyan3Tom Bola
8 Jan 25 i`* For a 100th Time Fuck Stackexchange (Re: Honoring Raymond Smullyan)2Mild Shock
8 Jan 25 i `- Outdated Policy Nonsense by Stackexchange Farts (Was: For a 100th Time Fuck Stackexchange)1Mild Shock
9 Jan 25 `* RETRO Project Sebastian Borgeaud et al. - 7 Feb 2022 (Was: Honoring Raymond Smullyan)5Mild Shock
10 Jan 25  `* Prologers are hurt the most by LLMs (Re: RETRO Project Sebastian Borgeaud et al. - 7 Feb 2022)4Mild Shock
10 Jan 25   +* XAI is over and out (Re: Vectors are the new JSON)2Mild Shock
10 Jan 25   i`- Academia is retarded (Re: XAI is over and out)1Mild Shock
10 Jan 25   `- Vectors are the new JSON (Re: Prologers are hurt the most by LLMs)1Mild Shock

Haut de la page

Les messages affichés proviennent d'usenet.

NewsPortal