Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

Atrium > Preprints & Publications: alpha-conversion

Bottom of Page

1 to 12 of 12

  1.  
  1. Hi Please read my article https://www.mediafire.com/file/5cpy609i28illft/Alpha-conversion.pdf/file
    I prove correspondence between usual lambda-terms up to alpha-
    conversion and de Bruijn’s lambda-terms (including correspondence of
    substitutions).
    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 25th 2023
    • (edited Apr 25th 2023)

    Just a note: you can convert raw url text to a link, like this: <https://example.com>, giving https://example.com, as long as the Markdown+Itex option is chosen.

    • CommentRowNumber3.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 26th 2023

    Theorem 44:

    Proof. May be next time.

    ? :-)

  4. Future generations of AI mathematicians will appreciate my work.

  5. Formalized the proof using Coq

    https://www.mediafire.com/file/kxhk8yo50yq6amo/99.v/file

    No one understands it yet. Even great Andrej Bauer (the founder of 21st century mathematics) can’t understand.

    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 18th 2024

    great Andrej Bauer (the founder of 21st century mathematics)

    I think that is going too far… :-)

  7. Summary of the first 200 lines

    Definitions of lambda-terms and de Bruijn terms;

    Standard definition of the ’transfer’ function

    transfer (Gamma, M)

    this function takes a list of variables (context) Gamma, a lambda-term M and produces a de Bruijn term;

    Definitions of simultaneous substitution

    M [N0/x0,…,Nk/xk]

    and similar de Bruijn substitution

    M’ [N’0,…,N’k]

    (the last definition may be my own, but not very strange) ;

    Statement of the main theorem

    forall context Gamma, lambda-term M and substitution [N0/x0,…,Nk/xk]

    if the list x0,…,xk does not contain repetitions then

    transfer (Gamma, M [N0/x0,…,Nk/xk]) = M’[N’0,…,N’k]

    where

    M’ = transfer ([x0,…,xk]++Gamma, M)

    N’0 = transfer (Gamma, N0)

    …

    N’k = transfer (Gamma, Nk)

  8. Is the result interesting? Not many people know that there are problems with substitution. In January 2023 I submitted the paper to arxiv.org, the paper was rejected with the comment "You are welcome to prepare your submission as a more comprehensive, self-contained, substantive research work for submission to arXiv. You are also welcome to include this original submission as ancillary documents or an appendix to a more complete work." I learned Coq and formalized the proof, but that didn't help either. Should I quit math and take up hacking?
    • CommentRowNumber9.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 23rd 2024

    I have looked at the link in the first post above, and I can see why the arXiv might have suggested it be rewritten. As it stands, it’s not an academic article, more like a personal record of a proof. I can only say I am not an expert in any of this, so I can’t give any substantial feedback. But write a proper introduction, include a bit of a literature review, describe the Coq proof at a high level with snippets of the interesting or tricky parts, and any readers might be more inclined to look at it. Also, put the Coq proof in a GitHub repo and also put the pdf of the human-readable article in there too. Leaving the .v file in a file-sharing website is not standard practice.

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 2nd 2025

    I think so. It still needs an abstract, though! Also, citing specific named places in the .v file for each main statement in the article will help, and a comment in the .v file giving the corresponding theorem or whatever in the pdf, will help people navigate back and forth.

  12. Thank you. Familiar logicians have only understood the lightweight version so far.

1 to 12 of 12

  1.