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.logic
Subject: Outdated Policy Nonsense by Stackexchange Farts (Re: For a 100th Time
 Fuck Stackexchange)
Date: Wed, 8 Jan 2025 11:31:39 +0100
Message-ID: <vllk69$205fd$1@solani.org>
References: <vlkfq7$1vh4j$1@solani.org> <vlkrge$2dkpc$1@dont-email.me>
 <vllgli$2039r$1@solani.org> <vllhv5$2043g$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 8 Jan 2025 10:31:37 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2102765"; 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:Vo0QRL5hlUlptiGo+43N0KEIGlk=
In-Reply-To: <vllhv5$2043g$1@solani.org>
X-User-ID: eJwNwoEVRDEEBMCWxLKhnBP0X8K/N+Pg4btGp/n+9dENYHK49SjjK+sCu4NgyS+QaEOm4HUr6bf1RFWNqn5JchUH
Bytes: 5534
Lines: 148

Hi,

How it started (simple vision):

"Once you have a truly massive amount of information
integrated as knowledge, then the human-software
system will be superhuman, in the same sense that
mankind with writing is superhuman compared to
mankind before writing."
https://en.wikipedia.org/wiki/Douglas_Lenat#Quotes

Isn't a Q&A site also a human-software system?

How its going (outdated nonsense):

The content you provide must either be your own original
work, or your summary of the properly referenced work of others.
[...] Generative artificial intelligence tools are not
capable of citing the sources of knowledge used up to
the standards of the Stack Exchange network.
https://math.stackexchange.com/help/gen-ai-policy

LoL, they are morons. They don't understand
how LLM use RAG nowadays.

Was ist Retrieval-Augmented Generation (RAG)?
https://aws.amazon.com/de/what-is/retrieval-augmented-generation/

Bye

Mild Shock schrieb:
> Hi,
> 
> 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?
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Thats System F and not simple types. also
>> known as the polymorphic lambda-calculus
>> or second-order lambda-calculus, it is an
>>
>> extension of simply typed lambda-calculus.
>> But in simple types itself, th self application
>> x x has no type. You can try yourself:
>>
>> /* Typed Variable */
>> typeof(_:A, B) :-
>>     unify_with_occurs_check(A, B).
>> /* Modus Ponens */
>> typeof((S*T), B) :-
>>     typeof(S, (A -> B)),
>>     typeof(T, A).
>>
>> And then the query:
>>
>> ?- X=_:_, typeof((X*X), T).
>> false.
>>
>> The query will though succeed if you remove
>> the occurs check.
>>
>> Bye
>>
>> Julio Di Egidio schrieb:
>>> On 08/01/2025 01:10, Mild Shock wrote:
>>>> 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
>>>
>>> Define Smullyan.
>>>
>>>> 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?
>>>
>>> Let `F : forall (X Y : Type), X -> Y`, then we can
>>> (almost) write `F F`.  Simple seems simple, it just
>>> doesn't end well:
>>>
>>> ```coq
>>> (** There exists a function
>>>      from any type to any type! *)
>>> Axiom F : forall (X Y : Type), X -> Y.
>>>
>>> (** Any two types: might be False False if
>>>      that's all there is, an uninhabited type. *)
>>> Parameters (T U : Type).
>>>
>>> (** Now we can prove False. *)
>>> Definition absurd : False :=
>>>    F (T -> U) False (F T U).
>>> ```
>>>
>>> -Julio
>>>
>>
>