Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
veganism.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Veganism Social is a welcoming space on the internet for vegans to connect and engage with the broader decentralized social media community.

Administered by:

Server stats:

295
active users

veganism.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0-alpha.5

#LambdaCalculus

3 posts3 participants0 posts today
HoldMyType<p><span class="h-card" translate="no"><a href="https://mathstodon.xyz/@rzeta0" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>rzeta0</span></a></span> <br>Ofc <br>Kleene–Rosser paradox demonstrates a contradiction in untyped <a href="https://mathstodon.xyz/tags/lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdacalculus</span></a>: it's possible to construct a lambda expression (like k = λ x . ( ¬ ( x x ) ) k=λx.(¬(xx))) so that when it's applied to itself, you get k k = ¬ ( k k ) kk=¬(kk)—which is a logical contradiction. This showed that untyped lambda calculus isn't suitable as a foundation for mathematical logic. That won't type check in <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a></p>
HoldMyTypeIomonad is not magic , but nothing less than the magic
Tariq<p>Is this right?</p><p>For a type in λP</p><p>A:*, B:* ⊢ ∏ z: A. (∏ y:(∏ x:A.B).B) : *</p><p>the following is an inhabitant:</p><p>λ z:A . (λ y:(∏ x:A.B) . yz) </p><p>It's taken me 3 days to work out why I initially couldn't find an inhabitant. I've learned along the way. I hope the above is correct.</p><p><a href="https://mathstodon.xyz/tags/maths" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>maths</span></a> <a href="https://mathstodon.xyz/tags/cs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>cs</span></a> <a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>typetheory</span></a> <a href="https://mathstodon.xyz/tags/lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdacalculus</span></a></p>
HoldMyType<p>Higher order functions re L(ast(IFO)?<br><a href="https://mathstodon.xyz/tags/lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdacalculus</span></a></p>
Tariq<p>I'm struggling with what should be a simple structural induction proof.</p><p>Prove that there are no Γand N in λω such that \[Γ ⊢ \Box : N\] is derivable.</p><p>Help very welcome!</p><p><a href="https://cs.stackexchange.com/questions/173317/help-with-structural-induction-proof-that-Γ-⊢-box-n-is-not-derivable-in-λω" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cs.stackexchange.com/questions</span><span class="invisible">/173317/help-with-structural-induction-proof-that-Γ-⊢-box-n-is-not-derivable-in-λω</span></a></p><p><a href="https://mathstodon.xyz/tags/maths" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>maths</span></a> <a href="https://mathstodon.xyz/tags/cs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>cs</span></a> <a href="https://mathstodon.xyz/tags/lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdacalculus</span></a> <a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>typetheory</span></a></p>
Björn Gohla<p>Found this in Barendregt's definition of combinatory logic 😆 </p><p><a href="https://mathstodon.xyz/tags/lambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdaCalculus</span></a> <a href="https://mathstodon.xyz/tags/functionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>functionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>logic</span></a> <a href="https://mathstodon.xyz/tags/SPQR" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SPQR</span></a></p>
Artyom Bologov<p><span class="h-card" translate="no"><a href="https://merveilles.town/@neauoire" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>neauoire</span></a></span> inspired me with their idea of a <a href="https://merveilles.town/tags/UXN" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>UXN</span></a> book and I wondered what my book might be about. And then I realized! I already have a series of <a href="https://merveilles.town/tags/blogpost" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>blogpost</span></a>-s about <a href="https://merveilles.town/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a>, so I can just continue that and I'll have a book! Intention in place, I set to continue my gargantuan series of "Making Sense of Lambda Calculus" posts. So here's a (0-indexed) part 5, "Bring Computation to (Aggregate) Data":</p><p><a href="https://aartaka.me/lambda-5.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">aartaka.me/lambda-5.html</span><span class="invisible"></span></a></p><p><span class="h-card" translate="no"><a href="https://oldbytes.space/@amoroso" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>amoroso</span></a></span> <span class="h-card" translate="no"><a href="https://merveilles.town/@bouncepaw" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>bouncepaw</span></a></span> did you two read the previous episodes? How were they?</p>
Light<p>This is cool:<br><a href="https://tromp.github.io/cl/diagrams.html" rel="nofollow noopener" target="_blank"><span class="invisible">https://</span><span class="ellipsis">tromp.github.io/cl/diagrams.ht</span><span class="invisible">ml</span></a></p><p><a href="https://noc.social/tags/math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>math</span></a> <a href="https://noc.social/tags/lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdacalculus</span></a></p>
HoldMyType<p><a href="https://mathstodon.xyz/tags/python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>python</span></a> lets ypu instantiate a function anywhere and a ( recursive) function definition can be self contained and last i checked its notorious for its type checking <br><a href="https://mathstodon.xyz/tags/Lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lambdacalculus</span></a> wont let you do that unyil you give it the required fixed point function <br><a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>typetheory</span></a><br>Oh and fixed point need not be in R<br>Unlike rieman zeta ?<br>OTOH python wont spit potential Nonsense</p>
HoldMyType<p>term&nbsp;Q = λ1((λ11)(λλλλλ14(3(55)2)))1&nbsp;concatenates two copies of its input, proving that</p><p>KS(xx) ≤ ℓ(x) + 66Applying it to its own encoding gives a 132 bit&nbsp;quine:</p><p>U(blc(Q)&nbsp;blc(Q) : Nil) = blc(Q)&nbsp;blc(Q)<br><a href="https://mathstodon.xyz/tags/lambdacalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>lambdacalculus</span></a> <br><a href="https://tromp.github.io/cl/Binary_lambda_calculus.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">tromp.github.io/cl/Binary_lamb</span><span class="invisible">da_calculus.html</span></a></p>
Csepp 🌢<p>:neofox_owo: !<br>&gt; Forsp: A <a href="https://merveilles.town/tags/Forth" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Forth</span></a>+<a href="https://merveilles.town/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</span></a> Hybrid <a href="https://merveilles.town/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> Language<br><a href="https://xorvoid.com/forsp.html" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">xorvoid.com/forsp.html</span><span class="invisible"></span></a></p>
Artyom Bologov<p>In the spirit of (not-that-radical, unfortunately) openness (inspired by none other than <span class="h-card" translate="no"><a href="https://mas.to/@TodePond" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>TodePond</span></a></span>,) let me share a thing I've been quietly working on for the last couple of months: <a href="https://merveilles.town/tags/Lamber" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lamber</span></a>, my pure <a href="https://merveilles.town/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> -compiling <a href="https://merveilles.town/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> language inspired by <a href="https://merveilles.town/tags/Lua" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lua</span></a> and <a href="https://merveilles.town/tags/haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>haskell</span></a> </p><p><a href="https://github.com/aartaka/lamber" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/aartaka/lamber</span><span class="invisible"></span></a></p><p><a href="https://merveilles.town/tags/theWorkshop" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>theWorkshop</span></a></p>
José A. Alonso<p>Readings shared February 22, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/02/22-readings_shared_02-22-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/02/22-readings_shared_02-22-25</span></a> <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</span></a></p>
José A. Alonso<p>Lambda calculus and Lisp, part 2. <a href="https://babbagefiles.xyz/lambda-calculus-and-lisp-02-recursion/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">babbagefiles.xyz/lambda-calcul</span><span class="invisible">us-and-lisp-02-recursion/</span></a> <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</span></a></p>
José A. Alonso<p>Lambda calculus and Lisp, part 1. <a href="https://babbagefiles.xyz/lambda-calculus-and-lisp-01/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">babbagefiles.xyz/lambda-calcul</span><span class="invisible">us-and-lisp-01/</span></a> <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lisp</span></a></p>
José A. Alonso<p>Readings shared February 16, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/02/16-readings_shared_02-16-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/02/16-readings_shared_02-16-25</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Reasoning</span></a></p>
José A. Alonso<p>The relationship between category theory, lambda calculus, and functional programming in Haskell. ~ Antonio Montano. <a href="https://4m4.it/posts/category-theory-functional-programming-compositionality/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">4m4.it/posts/category-theory-f</span><span class="invisible">unctional-programming-compositionality/</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a></p>
tc<p><a href="https://mathstodon.xyz/tags/functionalprogramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>functionalprogramming</span></a> </p><p>Many people's vote for most <a href="https://mathstodon.xyz/tags/beautiful" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>beautiful</span></a> construct in <a href="https://mathstodon.xyz/tags/math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>math</span></a> is \[ e^{i\pi}+1=0. \]</p><p>Yeah, maybe. But I think a close contender (if you include the <a href="https://mathstodon.xyz/tags/CS" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CS</span></a> realm) is \[ \lambda b.\lambda e.eb . \]</p><p>This serves as the complete <a href="https://mathstodon.xyz/tags/Church" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Church</span></a> encoding of <a href="https://mathstodon.xyz/tags/exponentiation" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>exponentiation</span></a> in <a href="https://mathstodon.xyz/tags/LambdaCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LambdaCalculus</span></a>, driving home subtler points about <a href="https://mathstodon.xyz/tags/function" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>function</span></a> <a href="https://mathstodon.xyz/tags/mapping" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>mapping</span></a> and ordered pairs and the primacy of exponentiation over add/mult, both of which have uglier <a href="https://mathstodon.xyz/tags/LC" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LC</span></a> representations.</p><p><a href="https://en.wikipedia.org/wiki/Lambda_calculus#Arithmetic_in_lambda_calculus" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">en.wikipedia.org/wiki/Lambda_c</span><span class="invisible">alculus#Arithmetic_in_lambda_calculus</span></a></p>
VegansExploreLive feeds
About