Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Monday, 25-Nov-2024 03:51:07 JST julesh

   I wonder what's the computational power of untyped linear lambda calculus?

   Pretty sure it's not Turing complete, I don't think you can write a fixpoint combinator or any other kind of recursor without breaking linearity

   • Embed this notice
     James Wood (mudri@mathstodon.xyz)'s status on Monday, 25-Nov-2024 03:54:42 JST James Wood

     in reply to

     @julesh All untyped linear λ-calculus terms can be given a simple type. Just do Hindley-Milner type inference, and nothing can go wrong without multiple occurrences of a variable. (Conor taught me this.)

   • Embed this notice
     fl (fl@mathstodon.xyz)'s status on Monday, 25-Nov-2024 06:23:05 JST fl

     in reply to

     @julesh P-complete according to the 14th slides.

     https://indico.math.cnrs.fr/event/6181/contributions/4944/attachments/2640/3348/noam-cap20.pdf

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Monday, 25-Nov-2024 06:25:14 JST julesh

     in reply to

     • fl

     @fl Big if true