Most active commenters

    ←back to thread

    Show HN: Term-Lisp – A Lisp, based on pattern matching and term rewriting

    (github.com)
    56 points boris_m | 15 comments | 06 Nov 24 14:53 UTC | HN request time: 0.645s | source | bottom
    1. BoiledCabbage ◴[06 Nov 24 18:07 UTC] No.42066515[source]▶
    Term re-writing systems are a really interesting way of looking at computation.

    It completely abstracts away the concept of a machine, and it's simply translation as computation - but equally as powerful.

    replies(3): >>42066655 #>>42066678 #>>42067446 #
    2. simplify ◴[06 Nov 24 18:16 UTC] No.42066655[source]▶
    Agreed. This reminds me – and I wonder if it could be applied – to Computational Type Theory, which relies on a similar concept of "reducing" types to their primitive forms, actually taking computation into account (something type theories normally do not!)

    This lecture series goes into how it works: https://www.youtube.com/watch?v=LE0SSLizYUI

    replies(1): >>42072875 #
    3. llm_trw ◴[06 Nov 24 18:17 UTC] No.42066678[source]▶
    It's a shame the standard texts are all 20 years old or more than way too heavy mathematically.

    A little book for term rewriting would be a great new addition.

    replies(1): >>42067199 #
    4. entaloneralie ◴[06 Nov 24 18:45 UTC] No.42067199[source]▶
    Here's a little zine on multiset rewriting(unordered term rewriting), John Conway said(about Fractran in The Book of Numbers) that it is such a simple paradigm of computation that no book is needed to learn it, and it can be taught in 10 seconds.

    https://wiki.xxiivv.com/site/pocket_rewriting

    replies(1): >>42069293 #
    5. lo_zamoyski ◴[06 Nov 24 18:59 UTC] No.42067446[source]▶
    I would argue that it is more "primordial". After all, computation is first and foremost a human activity, generally performed using pen and paper, which involves a good deal of rewriting (computers were originally people). The machine only came later as a way to simulate this human activity. Its meaning is entirely contingent on the primordial notion. It have no meaning on its own.
    replies(1): >>42070162 #
    6. BoiledCabbage ◴[06 Nov 24 20:59 UTC] No.42069293{3}[source]▶
    I'm somewhat surprised there isn't a semi-mainstream language for it. It's incredibly simple, with very few core concepts yet very powerful.

    Similar to LISP in that sense.

    replies(5): >>42069569 #>>42069855 #>>42070879 #>>42071115 #>>42072164 #
    7. Jtsummers ◴[06 Nov 24 21:19 UTC] No.42069569{4}[source]▶
    https://www.researchgate.net/publication/243768023_Mathemati...

    Mathematica is at least semi-mainstream. Not sure of any other examples though.

    8. entaloneralie ◴[06 Nov 24 21:38 UTC] No.42069855{4}[source]▶
    Maude is the most famous one that I know of I think.

    https://maude.lcc.uma.es/maude-manual/maude-manualch1.html#x...

    9. practal ◴[06 Nov 24 22:01 UTC] No.42070162[source]▶
    Of course term rewriting has a meaning of its own, it is at the same time more meaningful and simpler as any other form of computation.
    10. opminion ◴[06 Nov 24 22:58 UTC] No.42070879{4}[source]▶
    The foundations of Wolfram Language (Mathematica) are about transformations on symbolic expressions, at least conceptually.
    11. alxmng ◴[06 Nov 24 23:21 UTC] No.42071115{4}[source]▶
    I think the issue is performance. A true term rewriting system has to essentially operate on text, right?
    replies(2): >>42071220 #>>42071290 #
    12. Jtsummers ◴[06 Nov 24 23:30 UTC] No.42071220{5}[source]▶
    No, it can operate on a data structure as well. There's string rewriting which does operate on text (but this can be stored in a structure amenable to applying rewrite rules versus brute force copying it or something silly). For term rewriting, there are plenty of efficient ways to store and operate on the information besides just textually.
    13. simplify ◴[06 Nov 24 23:37 UTC] No.42071290{5}[source]▶
    Not necessarily, I would think terms can be converted to numbers like how the Ruby vm compiles symbols.
    14. UncleOxidant ◴[07 Nov 24 01:12 UTC] No.42072164{4}[source]▶
    There's Pure, but it's not exactly mainstream: https://agraef.github.io/pure-lang/
    15. deterministic ◴[07 Nov 24 02:55 UTC] No.42072875[source]▶
    I watched all 5 videos a few years ago. And if I understand it correctly "Computational Type Theory" basically defines a type as describing the behaviour of a computation.

    Which is really interesting but kinda hard for me to wrap my arms around compared with Martin Loff type theory. It looks as if type checking will have to be done manual, using N axiomatic rules for how you can prove A from B.

    Is that your understanding as well?

    Also, there doesn't seem to be much material on Computational Type theory online. Any good references? (Except for the nuPrl book of course).