Lambda Calculus Generator

The name of the pictureThe name of the pictureThe name of the pictureClash Royale CLAN TAG#URR8PPP











up vote
2
down vote

favorite












I don't know where else to ask this question, I hope this is a good place.



I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite time, produce every possible lambda calculus function. (like in the form of a string).



Since lambda calculus is so simple, having only a few elements to its notation I thought it might be possible (though, not very useful) to produce all possible combinations of that notation elements, starting with the simplest combinations, and thereby produce every possible lambda calculus function.



Of course, I know almost nothing about lambda calculus so I have no idea if this is really possible.



Is it? If so, is it pretty straightforward like I've envisioned it, or is it technically possible, but so difficult that it is effectively impossible?



PS. I'm not talking about beta-reduced functions, I'm just talking about every valid notation of every lambda calculus function.






lambda-calculus







share|cite|improve this question



























    up vote
    2
    down vote

    favorite












    I don't know where else to ask this question, I hope this is a good place.



    I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite time, produce every possible lambda calculus function. (like in the form of a string).



    Since lambda calculus is so simple, having only a few elements to its notation I thought it might be possible (though, not very useful) to produce all possible combinations of that notation elements, starting with the simplest combinations, and thereby produce every possible lambda calculus function.



    Of course, I know almost nothing about lambda calculus so I have no idea if this is really possible.



    Is it? If so, is it pretty straightforward like I've envisioned it, or is it technically possible, but so difficult that it is effectively impossible?



    PS. I'm not talking about beta-reduced functions, I'm just talking about every valid notation of every lambda calculus function.






    lambda-calculus







    share|cite|improve this question

























      up vote
      2
      down vote

      favorite









      up vote
      2
      down vote

      favorite











      I don't know where else to ask this question, I hope this is a good place.



      I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite time, produce every possible lambda calculus function. (like in the form of a string).



      Since lambda calculus is so simple, having only a few elements to its notation I thought it might be possible (though, not very useful) to produce all possible combinations of that notation elements, starting with the simplest combinations, and thereby produce every possible lambda calculus function.



      Of course, I know almost nothing about lambda calculus so I have no idea if this is really possible.



      Is it? If so, is it pretty straightforward like I've envisioned it, or is it technically possible, but so difficult that it is effectively impossible?



      PS. I'm not talking about beta-reduced functions, I'm just talking about every valid notation of every lambda calculus function.






      lambda-calculus







      share|cite|improve this question















      I don't know where else to ask this question, I hope this is a good place.



      I'm just curious to know if its possible to make a lambda calculus generator; essentially, a loop that will, given infinite time, produce every possible lambda calculus function. (like in the form of a string).



      Since lambda calculus is so simple, having only a few elements to its notation I thought it might be possible (though, not very useful) to produce all possible combinations of that notation elements, starting with the simplest combinations, and thereby produce every possible lambda calculus function.



      Of course, I know almost nothing about lambda calculus so I have no idea if this is really possible.



      Is it? If so, is it pretty straightforward like I've envisioned it, or is it technically possible, but so difficult that it is effectively impossible?



      PS. I'm not talking about beta-reduced functions, I'm just talking about every valid notation of every lambda calculus function.






      lambda-calculus




      lambda-calculus






      share|cite|improve this question















      share|cite|improve this question













      share|cite|improve this question




      share|cite|improve this question








      edited 8 hours ago

























      asked 8 hours ago









      Legit Stack

      1364




      1364




















          2 Answers
          2






          active

          oldest

          votes

















          up vote
          5
          down vote













          Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.






          share|cite|improve this answer




















          • Essentially, all problems like this are solved by invoking the typing monkey...
            – xuq01
            1 hour ago

















          up vote
          0
          down vote













          Sure, this is a standard encoding exercise.



          First of all, let $p : mathbb N^2 to mathbb N$ any bijective computable function, called a pairing function. A standard choice is



          $$
          p(n,m) = dfrac(n+m)(n+m+1)2+n
          $$



          One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$.



          To enumerate lambda terms, fix any enumeration for variables names: $x_0,x_1,x_2,ldots$.



          Then, for each natural number $i$, print $lambda(i)$, defined recursively as follows:



          • if $i$ is even, let $j=i/2$ and return variable $x_j$

          • if $i$ is odd, let $j=(i-1)/2$

            • if $j$ is even, let $k=j/2$ and find $n,m$ such that $p(n,m)=k$; compute $N=lambda(n), M=lambda(m)$; return application $(NM)$

            • if $j$ is odd, let $k=(j-1)/2$ and find $n,m$ such that $p(n,m)=k$; compute $M=lambda(m)$; return abstraction $(lambda x_n. M)$


          This program is constructed by the following "algebraic" bijection among lambda terms syntax:



          $$
          Lambda simeq mathbb N + Lambda^2 + mathbb N times Lambda
          $$



          which is read as "the lambda terms, syntactically, are the disjoint union of 1) variables (represented as a natural), 2) applications (make by two lambda terms), and 3) abstraction (a pair variable/natural + lambda term)".



          Given that, we recursively apply computable bijections $mathbb N^2 simeq mathbb N$ ($p$) and $mathbb N + mathbb N simeq mathbb N$ (the standard even/odd one) to obtain the algorithm above.



          This procedure is general, and will work on almost any language generated through a context-free grammar, which will provide a similar isomorphism to the one above.






          share|cite




















            Your Answer




            StackExchange.ifUsing("editor", function ()
            return StackExchange.using("mathjaxEditing", function ()
            StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
            StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
            );
            );
            , "mathjax-editing");

            StackExchange.ready(function()
            var channelOptions =
            tags: "".split(" "),
            id: "419"
            ;
            initTagRenderer("".split(" "), "".split(" "), channelOptions);

            StackExchange.using("externalEditor", function()
            // Have to fire editor after snippets, if snippets enabled
            if (StackExchange.settings.snippets.snippetsEnabled)
            StackExchange.using("snippets", function()
            createEditor();
            );

            else
            createEditor();

            );

            function createEditor()
            StackExchange.prepareEditor(
            heartbeatType: 'answer',
            convertImagesToLinks: false,
            noModals: false,
            showLowRepImageUploadWarning: true,
            reputationToPostImages: null,
            bindNavPrevention: true,
            postfix: "",
            onDemand: true,
            discardSelector: ".discard-answer"
            ,immediatelyShowMarkdownHelp:true
            );



            );













             

            draft saved


            draft discarded


















            StackExchange.ready(
            function ()
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f97539%2flambda-calculus-generator%23new-answer', 'question_page');

            );

            Post as a guest

















            2 Answers
            2






            active

            oldest

            votes








            2 Answers
            2






            active

            oldest

            votes









            active

            oldest

            votes






            active

            oldest

            votes








            up vote
            5
            down vote













            Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.






            share|cite|improve this answer




















            • Essentially, all problems like this are solved by invoking the typing monkey...
              – xuq01
              1 hour ago














            up vote
            5
            down vote













            Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.






            share|cite|improve this answer




















            • Essentially, all problems like this are solved by invoking the typing monkey...
              – xuq01
              1 hour ago












            up vote
            5
            down vote










            up vote
            5
            down vote









            Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.






            share|cite|improve this answer












            Yes. Take something that enumerates all possible ASCII strings. For each output, check if it is a valid lambda calculus syntax that defines a function; if not, skip it. (That check can be done.) That enumerates all lambda calculus functions.







            share|cite|improve this answer












            share|cite|improve this answer



            share|cite|improve this answer










            answered 3 hours ago









            D.W.♦

            96.2k11111260




            96.2k11111260











            • Essentially, all problems like this are solved by invoking the typing monkey...
              – xuq01
              1 hour ago
















            • Essentially, all problems like this are solved by invoking the typing monkey...
              – xuq01
              1 hour ago















            Essentially, all problems like this are solved by invoking the typing monkey...
            – xuq01
            1 hour ago




            Essentially, all problems like this are solved by invoking the typing monkey...
            – xuq01
            1 hour ago










            up vote
            0
            down vote













            Sure, this is a standard encoding exercise.



            First of all, let $p : mathbb N^2 to mathbb N$ any bijective computable function, called a pairing function. A standard choice is



            $$
            p(n,m) = dfrac(n+m)(n+m+1)2+n
            $$



            One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$.



            To enumerate lambda terms, fix any enumeration for variables names: $x_0,x_1,x_2,ldots$.



            Then, for each natural number $i$, print $lambda(i)$, defined recursively as follows:



            • if $i$ is even, let $j=i/2$ and return variable $x_j$

            • if $i$ is odd, let $j=(i-1)/2$

              • if $j$ is even, let $k=j/2$ and find $n,m$ such that $p(n,m)=k$; compute $N=lambda(n), M=lambda(m)$; return application $(NM)$

              • if $j$ is odd, let $k=(j-1)/2$ and find $n,m$ such that $p(n,m)=k$; compute $M=lambda(m)$; return abstraction $(lambda x_n. M)$


            This program is constructed by the following "algebraic" bijection among lambda terms syntax:



            $$
            Lambda simeq mathbb N + Lambda^2 + mathbb N times Lambda
            $$



            which is read as "the lambda terms, syntactically, are the disjoint union of 1) variables (represented as a natural), 2) applications (make by two lambda terms), and 3) abstraction (a pair variable/natural + lambda term)".



            Given that, we recursively apply computable bijections $mathbb N^2 simeq mathbb N$ ($p$) and $mathbb N + mathbb N simeq mathbb N$ (the standard even/odd one) to obtain the algorithm above.



            This procedure is general, and will work on almost any language generated through a context-free grammar, which will provide a similar isomorphism to the one above.






            share|cite
























              up vote
              0
              down vote













              Sure, this is a standard encoding exercise.



              First of all, let $p : mathbb N^2 to mathbb N$ any bijective computable function, called a pairing function. A standard choice is



              $$
              p(n,m) = dfrac(n+m)(n+m+1)2+n
              $$



              One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$.



              To enumerate lambda terms, fix any enumeration for variables names: $x_0,x_1,x_2,ldots$.



              Then, for each natural number $i$, print $lambda(i)$, defined recursively as follows:



              • if $i$ is even, let $j=i/2$ and return variable $x_j$

              • if $i$ is odd, let $j=(i-1)/2$

                • if $j$ is even, let $k=j/2$ and find $n,m$ such that $p(n,m)=k$; compute $N=lambda(n), M=lambda(m)$; return application $(NM)$

                • if $j$ is odd, let $k=(j-1)/2$ and find $n,m$ such that $p(n,m)=k$; compute $M=lambda(m)$; return abstraction $(lambda x_n. M)$


              This program is constructed by the following "algebraic" bijection among lambda terms syntax:



              $$
              Lambda simeq mathbb N + Lambda^2 + mathbb N times Lambda
              $$



              which is read as "the lambda terms, syntactically, are the disjoint union of 1) variables (represented as a natural), 2) applications (make by two lambda terms), and 3) abstraction (a pair variable/natural + lambda term)".



              Given that, we recursively apply computable bijections $mathbb N^2 simeq mathbb N$ ($p$) and $mathbb N + mathbb N simeq mathbb N$ (the standard even/odd one) to obtain the algorithm above.



              This procedure is general, and will work on almost any language generated through a context-free grammar, which will provide a similar isomorphism to the one above.






              share|cite






















                up vote
                0
                down vote










                up vote
                0
                down vote









                Sure, this is a standard encoding exercise.



                First of all, let $p : mathbb N^2 to mathbb N$ any bijective computable function, called a pairing function. A standard choice is



                $$
                p(n,m) = dfrac(n+m)(n+m+1)2+n
                $$



                One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$.



                To enumerate lambda terms, fix any enumeration for variables names: $x_0,x_1,x_2,ldots$.



                Then, for each natural number $i$, print $lambda(i)$, defined recursively as follows:



                • if $i$ is even, let $j=i/2$ and return variable $x_j$

                • if $i$ is odd, let $j=(i-1)/2$

                  • if $j$ is even, let $k=j/2$ and find $n,m$ such that $p(n,m)=k$; compute $N=lambda(n), M=lambda(m)$; return application $(NM)$

                  • if $j$ is odd, let $k=(j-1)/2$ and find $n,m$ such that $p(n,m)=k$; compute $M=lambda(m)$; return abstraction $(lambda x_n. M)$


                This program is constructed by the following "algebraic" bijection among lambda terms syntax:



                $$
                Lambda simeq mathbb N + Lambda^2 + mathbb N times Lambda
                $$



                which is read as "the lambda terms, syntactically, are the disjoint union of 1) variables (represented as a natural), 2) applications (make by two lambda terms), and 3) abstraction (a pair variable/natural + lambda term)".



                Given that, we recursively apply computable bijections $mathbb N^2 simeq mathbb N$ ($p$) and $mathbb N + mathbb N simeq mathbb N$ (the standard even/odd one) to obtain the algorithm above.



                This procedure is general, and will work on almost any language generated through a context-free grammar, which will provide a similar isomorphism to the one above.






                share|cite












                Sure, this is a standard encoding exercise.



                First of all, let $p : mathbb N^2 to mathbb N$ any bijective computable function, called a pairing function. A standard choice is



                $$
                p(n,m) = dfrac(n+m)(n+m+1)2+n
                $$



                One can prove that this is a bijection, so given any natural $k$, we can compute $n,m$ such that $p(n,m)=k$.



                To enumerate lambda terms, fix any enumeration for variables names: $x_0,x_1,x_2,ldots$.



                Then, for each natural number $i$, print $lambda(i)$, defined recursively as follows:



                • if $i$ is even, let $j=i/2$ and return variable $x_j$

                • if $i$ is odd, let $j=(i-1)/2$

                  • if $j$ is even, let $k=j/2$ and find $n,m$ such that $p(n,m)=k$; compute $N=lambda(n), M=lambda(m)$; return application $(NM)$

                  • if $j$ is odd, let $k=(j-1)/2$ and find $n,m$ such that $p(n,m)=k$; compute $M=lambda(m)$; return abstraction $(lambda x_n. M)$


                This program is constructed by the following "algebraic" bijection among lambda terms syntax:



                $$
                Lambda simeq mathbb N + Lambda^2 + mathbb N times Lambda
                $$



                which is read as "the lambda terms, syntactically, are the disjoint union of 1) variables (represented as a natural), 2) applications (make by two lambda terms), and 3) abstraction (a pair variable/natural + lambda term)".



                Given that, we recursively apply computable bijections $mathbb N^2 simeq mathbb N$ ($p$) and $mathbb N + mathbb N simeq mathbb N$ (the standard even/odd one) to obtain the algorithm above.



                This procedure is general, and will work on almost any language generated through a context-free grammar, which will provide a similar isomorphism to the one above.







                share|cite












                share|cite



                share|cite










                answered 5 mins ago









                chi

                10.2k1627




                10.2k1627



























                     

                    draft saved


                    draft discarded















































                     


                    draft saved


                    draft discarded














                    StackExchange.ready(
                    function ()
                    StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f97539%2flambda-calculus-generator%23new-answer', 'question_page');

                    );

                    Post as a guest
































































                    Comments

                    Post a Comment

                    Popular posts from this blog

                    What does second last employer means? [closed]

                    Image
                    Clash Royale CLAN TAG #URR8PPP .everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty margin-bottom:0; up vote -3 down vote favorite Say, for example I have worked in the following companies, Company A => 2010 - 2011 Company B => 2011 - 2012 Company C => 2012 - Till Date Company D => Have offer Now assume Company D is asking to submit documents from my second last employer. So from the list of companies given, which company would be qualified as second last employer? software-industry employer share | improve this question asked Aug 10 '14 at 5:16 Rajaprabhu Aravindasamy 559 1 6 13 closed as off-topic by Jim G., jmort253 ♦ Aug 11 '14 at 1:58 This question appears to be off-topic. The users who voted to close gave this specific reason: "Questions seeking advice on company-specific regulations, agreements, or policies should be directed to your manager or HR department. Questions that address...
                    Read more

                    List of Gilmore Girls characters

                    Image
                    The season three cast—(Back row): Lane, Michel, Paris, Emily, Richard, Sookie, Miss Patty, Kirk; Front row: Jess, Luke, Lorelai, Rory, Dean This is a list of characters for the comedy-drama television series Gilmore Girls . Contents 1 Main characters 1.1 Lorelai Gilmore 1.2 Rory Gilmore 1.3 Sookie St. James 1.4 Lane Kim 1.5 Michel Gerard 1.6 Luke Danes 1.7 Emily Gilmore 1.8 Richard Gilmore 1.9 Paris Geller 1.10 Dean Forester 1.11 Jess Mariano 1.12 Kirk Gleason 1.13 Jason Stiles 1.14 Logan Huntzberger 2 Major recurring characters 2.1 Christopher Hayden 2.2 Jackson Belleville 2.3 Mrs. Kim 2.4 Tristin DuGray 2.5 Max Medina 2.6 Taylor Doose 2.7 Dave Rygalski 2.8 Marty 3 Recurring characters 3.1 Stars Hollow 3.2 Chilton 3.3 Yale 3.4 Other 4 Notable guest stars 5 Unseen characters 6 Notes 7 References Main characters Actor Character Appearances Season 1 Season 2 Season 3 Season 4 Season 5 Season 6 Season 7 A Year in the Life Lauren Graham Lorelai Gilmore...
                    Read more

                    Confectionery

                    Image
                    Prepared foods made with a lot of sugar or other cabohydrates "Sweetmeat" redirects here. For the racehorse, see Sweetmeat (horse). Not to be confused with Sweetbread. This Kransekake is a traditional Scandinavian baker's confection. Confectionery is the art of making confections , which are food items that are rich in sugar and carbohydrates. Exact definitions are difficult. [1] In general, though, confectionery is divided into two broad and somewhat overlapping categories, bakers' confections and sugar confections. [2] Bakers' confectionery, also called flour confections , includes principally sweet pastries, cakes, and similar baked goods. Sugar confectionery includes candies ( sweets in British English), candied nuts, chocolates, chewing gum, bubble gum, pastillage, and other confections that are made primarily of sugar. In some cases, chocolate confections (confections made of chocolate) are treated as a separate category, as are sugar-free versions of ...
                    Read more