• =?UTF-8?Q?Accelerate_Lean!_From_Theorem_3.11_to_Corollary_3.12_[ZMC?= =?UTF-8?Q?]_=28Was:_Introduction_to_AI_Accelerator_Prolog_[=cf=80-WAM_of_Do?= =?UTF-8?Q?gelog]=29?=

    From Mild Shock@janburse@fastmail.fm to comp.lang.prolog,sci.logic,sci.math on Sun Jul 19 16:06:21 2026
    From Newsgroup: sci.logic

    Hi,

    Accelerate Lean! And get from Theorem 3.11
    to Corollary 3.12 done.

    PROJECT LANA INTERIM REPORT ON IUT THEORY
    ZEN Mathematics Center - 2026/07/17
    https://zen.ac.jp/en/zmc

    ZMCN+eZEN Mathematics Center) is an international
    research institute established with the aim
    of promoting and developing modern mathematics

    with a focus on arithmetic geometry and the
    formalization of modern mathematics using
    computer languages

    LoL

    Bye

    Mild Shock schrieb:
    Hi,

    Maybe I should write a blog post, titled
    Introduction to AI Accelerator Prolog:

    - specialized jobs -C-WAM (currently integerish stuff)
    - -C-WAM uses no atomics, only comms
    - -C-WAM uses warp, 30-40% more speed
    - -C-WAM runs on GPU and CPU
    - -C-WAM runs from within JavaScript, Python and Java

    Feels like reinventing FGCS concurrent
    logic programming.

    LoL

    Bye

    Mild Shock schrieb:
    Hi,

    So the idea is to cover backtracking without
    stack and choice points, only with registers.
    So at the compute goto will use an instruction

    that stores the PC target into a register,
    a new instruction for Hack:

    -a-a-a REG = PC + REL

    And then the jump will be, again a new
    instruction for Hack:

    -a-a-a PC = REG

    If we squeeze the lemon and compile as much
    with that, we will only find that it breaks for
    calling recursive predicates that can use

    arbitary registers and choice points. But we
    could maybe add stack and choice point as an
    after match, instead of the classical WAM design

    that starts with stack and choice points!

    Bye

    Mild Shock schrieb:
    Hi,

    pi-WAM is a nice challenge, since its aim is to go
    even blow the instruction set of SWI-Prolog,
    while only using a Hack variant as instruction

    stream. But what is Hack? Well Hack seems to be
    the missing legacy of Niclaus Wirths PL0. The
    Hack (machine .asm) and Jack (highlevel compiler

    generating .vm which can be converted to .asm)
    combo makes even the famous Crafting Interpreters
    /Lox by Bob Nystrom redundant:

    Nand to Tetris courses are taught at 400+
    universities, high schools, and bootcamps. The
    students who take them range from high
    schoolers to Ph.D. students to
    https://www.nand2tetris.org/

    But digging deaper in Hack, it has no functions
    pointers so objects don't use virtual tables.
    But what will pi-WAM need and that is not yet

    in Hack? Given that my pi-WAM doesn't want a stack
    nor a choice point lists? Currently there is the
    idea to add a computed goto and that it can

    cover a more lightweight C_OR as known from
    SWI-Prolog, that would have the C_OR branches
    maybe restricted to have no outside

    clause calls? Lets see. Not yet sure.

    Bye


    --- Synchronet 3.22a-Linux NewsLink 1.2
  • From Mild Shock@janburse@fastmail.fm to comp.lang.prolog,sci.logic,sci.math on Sun Jul 19 16:21:57 2026
    From Newsgroup: sci.logic

    Hi,

    While some logicians seem to go backwards,
    bascially want GPUs eliminated from laptops,
    and then kill any windows manager, just use EXWM:

    From XFCE to EXWM
    Emacs is a text editor that, through EXWM (Emacs X
    Window Manager), can also be your window manager: https://www.vidal-rosset.net/2026-07-12-from-xfce-to-exwm-living-in-emacs-desktop-on-mx-linux.html

    Mostlikely we might soon see the backward
    sequel to E-graphs called EMACS-graphs. But
    here is my proposal, why not go the other way?

    - -C-E-graphs: Basically parallel E-graphs
    - Pegg: An alternative egg library, using -C-WAM

    Ok, this will not come so fast. Currently
    my -C-WAM is still very integerish. Not
    sure how to do anything E-graph yet.

    Bye

    P.S: There is already an attempt based on
    Scala 3.4.1, some experiments done on
    Intel Core i7-12700K using 8 threads.

    But why use a very old CPU from Q4'21,
    when you can use an AI Laptop from 2026
    with 512 GPU streaming processors?

    Parallel and Customizable Equality Saturation https://dl.acm.org/doi/pdf/10.1145/3771775.3786266

    Mild Shock schrieb:
    Hi,

    Accelerate Lean! And get from Theorem 3.11
    to Corollary 3.12 done.

    PROJECT LANA INTERIM REPORT ON IUT THEORY
    ZEN Mathematics Center - 2026/07/17
    https://zen.ac.jp/en/zmc

    ZMCN+eZEN Mathematics Center) is an international
    research institute established with the aim
    of promoting and developing modern mathematics

    with a focus on arithmetic geometry and the
    formalization of modern mathematics using
    computer languages

    LoL

    Bye

    Mild Shock schrieb:
    Hi,

    Maybe I should write a blog post, titled
    Introduction to AI Accelerator Prolog:

    - specialized jobs -C-WAM (currently integerish stuff)
    - -C-WAM uses no atomics, only comms
    - -C-WAM uses warp, 30-40% more speed
    - -C-WAM runs on GPU and CPU
    - -C-WAM runs from within JavaScript, Python and Java

    Feels like reinventing FGCS concurrent
    logic programming.

    LoL

    Bye

    Mild Shock schrieb:
    Hi,

    So the idea is to cover backtracking without
    stack and choice points, only with registers.
    So at the compute goto will use an instruction

    that stores the PC target into a register,
    a new instruction for Hack:

    -a-a-a REG = PC + REL

    And then the jump will be, again a new
    instruction for Hack:

    -a-a-a PC = REG

    If we squeeze the lemon and compile as much
    with that, we will only find that it breaks for
    calling recursive predicates that can use

    arbitary registers and choice points. But we
    could maybe add stack and choice point as an
    after match, instead of the classical WAM design

    that starts with stack and choice points!

    Bye

    Mild Shock schrieb:
    Hi,

    pi-WAM is a nice challenge, since its aim is to go
    even blow the instruction set of SWI-Prolog,
    while only using a Hack variant as instruction

    stream. But what is Hack? Well Hack seems to be
    the missing legacy of Niclaus Wirths PL0. The
    Hack (machine .asm) and Jack (highlevel compiler

    generating .vm which can be converted to .asm)
    combo makes even the famous Crafting Interpreters
    /Lox by Bob Nystrom redundant:

    Nand to Tetris courses are taught at 400+
    universities, high schools, and bootcamps. The
    students who take them range from high
    schoolers to Ph.D. students to
    https://www.nand2tetris.org/

    But digging deaper in Hack, it has no functions
    pointers so objects don't use virtual tables.
    But what will pi-WAM need and that is not yet

    in Hack? Given that my pi-WAM doesn't want a stack
    nor a choice point lists? Currently there is the
    idea to add a computed goto and that it can

    cover a more lightweight C_OR as known from
    SWI-Prolog, that would have the C_OR branches
    maybe restricted to have no outside

    clause calls? Lets see. Not yet sure.

    Bye



    --- Synchronet 3.22a-Linux NewsLink 1.2