• edinbruh@feddit.itEnglish
    24·
    2 天前

    Oooooohhh! That’s my field of study!

    So, you know how in programming you have data types (like int, float, structs etc…) well, they are actually math.

    In math, more specifically in logics, there’s these things called “judgement derivation systems”. They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.

    You see, one day Mr Howard wrote to Mr Curry: “I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction” and curry answered: “wow, that’s cool, I’ll tell you more, a type system for this other thing kinda looks like combinatory logics” and then they both went “could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?” And this is what modern type theory (and theorem provers) are based on.

    Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a “context” object, which is often identified with the letter gamma.

      • edinbruh@feddit.itEnglish
        6·
        1 天前

        I was aware of that, but I didn’t want to do a full write-up from zero knowledge to type theory…

        Maybe I’ll do it later tho. Because I enjoy explaining this stuff.

        Anyway, despite the comedic delivery, that comment should give a 1st year CS student all the keywords they need to research the subject. Especially the letters between Curry and Howard, which are referred to as the “Curry-Howard correspondence”

        • strawberry_enjoyer42@lemmy.blahaj.zoneEnglish
          3·
          24 小时前

          I was joking, a bit. It’s not like you can explain all of it in one random comment.

          Aghhh! I wanna get a cs degree, but I had to switch programs for r e a s o n s. Maybe I could get one after my associate’s degree.

  • maria [she/her]@lemmy.blahaj.zoneEnglish
    7·
    2 天前

    everything hits the tokenizer at some point 💀 which is where all data meets their maker.

    • a palm tree? 🌴 oh u mean generic tree with fancy leaves? 🌳❇️
    • a chair? 🪑 oh u mean symbols arranged chair-wise?
    • a heartfelt message to your crush? 💖 oh u mean char[]? (characters stringed together in a sequence)
    • a wonderful picture? u mean a list of colors and a columns count?

    everything loses detail after the tokenizer.

    • lfox02@lemmy.blahaj.zoneEnglish
      2·
      22 小时前

      Behold, a man! - ChatGPT

      a wonderful picture? u mean a list of colors and a columns count?

      Isn’t that all digital photography anyway?

        • lfox02@lemmy.blahaj.zoneEnglish
          1·
          4 小时前

          The joke is a cross between a famous anecdote about Diogenes and the inner workings of vision-capable AI models.

          Diogenes really liked to disrespect his social superiors, so when, in a lecture, Plato defined human beings as “featherless bipeds”, Diogenes plucked a chicken and presented it to him saying “Behold - Plato’s human being” (or something along those lines, the quote is slightly different in every source).

          In order to “see” things from images and video, a garden variety LLM needs to integrate with another model that analyzes the picture it is given and gives a text description (source: HuggingFace). What I’m getting at is that, based on that idea of stripping things of context, ChatGPT could probably confidently tell you something in the vein of Plato taking the piss due to its inherently limited ability to see.

          • maria [she/her]@lemmy.blahaj.zoneEnglish
            1·
            3 小时前

            oh wowie no way someone did the reading on HUGGINGFACE??? wowie, never expected that link to make it to 196…

            anyway: good joke, i get it now, thank u.