5 ms·

It's a stripped down model of computation like the SKI calculus [0] or its cousin the lambda calculus, which are formal systems with precise rules for mechanica

by ryandv 2y ago

It's a stripped down model of computation like the SKI calculus [0] or its cousin the lambda calculus, which are formal systems with precise rules for mechanically evaluating or reducing expressions. It differs from the SKI calculus in that it can reflect on its own program structure, especially in ways the SKI calculus cannot - deciding if two programs are equal, for instance [1]. Further, unlike the lambda calculus, reducing a program with the reduction rules given [2] eventually converges upon a stable "normal form" of the program, which is expressed in irreducible terms, instead of leading to possibly infinite chains of reduction [3]. This allows for reflection without needing to "quote" or serialize the program into a stable data structure or other representation to sidestep the possibility of infinite reduction. This is similar to the notion of homoiconicity as in Lisp. [0] https://en.wikipedia.org/wiki/SKI_combinator_calculus https://en.wikipedia.org/wiki/SKI_combinator_calculus [1] https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf https://github.com/barry-jay-personal/tree-calculus/blob/mas... [2] https://treecalcul.us/specification/ https://treecalcul.us/specification/ [3] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs.2019.02.016 https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....

cjfd 2y ago
"reducing a program with the reduction rules given eventually converges upon a stable "normal form" of the program". How is that possible if the reduction rules define a Turing complete language?
- ryandv 2y ago
  It would appear that programs in even SKI calculus and other combinatory logics can reduce to base combinators in finitely many steps, but when those combinators are applied to arguments, then the possibility of non-termination arises [0]: Combinatory logic [9,12] is very close to λ-calculus, and widely considered to be equivalent to it [8], but there are important differences. In particular, by modifying the usual account of recursion, i.e. by modifying the usual account of fixpoint functions, it is possible to ensure that all programs are represented by stable combinators, i.e. combinators that are irreducible or in normal form. Only when applied to arguments does non-termination become possible. That is, we may define a program to be a combinator in normal form. As such it is both an executable, since applications of it will trigger evaluation, and also a syntax tree, i.e. a binary tree of applications, with leaves labelled by the primitive combinators, say S and K. [0] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs.2019.02.016 https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
  - chriswarbo 2y ago
    This thread is perhaps phrased confusingly. If I understand correctly, the claim is only that any program (including recursive ones) can be expressed in a finite normal form, which may of course diverge when "run" (applied to an argument). The same is true for basically every language though, e.g. consider the following Python: omega = lambda x: x(x) omega(omega)(42) The expression `omega(omega)` diverges, but only because we've applied it to an argument. The function `omega` itself is in an irreducible normal form, namely `lambda x: x(x)`. On the other hand, consider the function call with argument `42`: in that case, the function is `omega(omega)`, which is not in a normal form, and in fact diverges. In a system like SK, and presumably this tree calculus, we can form a similar expression, where the "function part" (i.e. left sub-tree) diverges with no normal form. That's unavoidable, due to the halting problem. I think the claim is that we never need to write such expressions, since there's always an alternative which behaves the same but whose "function part" has a normal form. As a (slightly) more practical example, consider some code like: adjust = (lambda x: x + 1) if increase else (lambda x: x - 1) The function `adjust` is not in a normal form, since it depends on the value of `increase` (when truthy, `adjust` will increment; when falsy it'll decrement). Yet most programmers would probably avoid that, in favour of this: adjust = lambda x: x + 1 if increase else x - 1 Both implementations of `adjust` will behave the same, but the second is in a normal form.
    - calf 2y ago
      I'm rusty but doesn't the increase depend differently, the second adjust lets you decide to assign a value for the variable increase much later, whereas the first adjust fixes the value of increase at the point of evaluating that very assignment statement. There's a name for this, dynamic scoping or something.
      - smsm42 2y ago
        Yes, the two are not identical - in the former, increase is not the part of the closure, in the latter it is. Test: increase = True adjust1 = (lambda x: x + 1) if increase else (lambda x: x - 1) adjust2 = lambda x: x + 1 if increase else x - 1 print(adjust1(42)) print(adjust2(42)) increase = False print(adjust1(42)) print(adjust2(42))
__MatrixMan__ 2y ago
Thanks for the links, I'll be reading up on these. When I signed up for a computer science degree, I was hoping I'd learn this stuff (if not this calculus, than enough context to grapple with it at least). What I actually got was software engineering. Snore.
- calf 2y ago
  The Theoretical Programming Languages class I took for my minor at Princeton was okay, basically they just taught from Benjamin Pierce's textbook. I'm sure there are other undergrad level intro class syllabi available if that's something you have spare time to self study.

by ryandv 2y ago

cjfd 2y ago

"reducing a program with the reduction rules given eventually converges upon a stable "normal form" of the program". How is that possible if the reduction rules define a Turing complete language?

ryandv 2y ago
It would appear that programs in even SKI calculus and other combinatory logics can reduce to base combinators in finitely many steps, but when those combinators are applied to arguments, then the possibility of non-termination arises [0]: Combinatory logic [9,12] is very close to λ-calculus, and widely considered to be equivalent to it [8], but there are important differences. In particular, by modifying the usual account of recursion, i.e. by modifying the usual account of fixpoint functions, it is possible to ensure that all programs are represented by stable combinators, i.e. combinators that are irreducible or in normal form. Only when applied to arguments does non-termination become possible. That is, we may define a program to be a combinator in normal form. As such it is both an executable, since applications of it will trigger evaluation, and also a syntax tree, i.e. a binary tree of applications, with leaves labelled by the primitive combinators, say S and K. [0] https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs.2019.02.016 https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
- chriswarbo 2y ago
  This thread is perhaps phrased confusingly. If I understand correctly, the claim is only that any program (including recursive ones) can be expressed in a finite normal form, which may of course diverge when "run" (applied to an argument). The same is true for basically every language though, e.g. consider the following Python: omega = lambda x: x(x) omega(omega)(42) The expression `omega(omega)` diverges, but only because we've applied it to an argument. The function `omega` itself is in an irreducible normal form, namely `lambda x: x(x)`. On the other hand, consider the function call with argument `42`: in that case, the function is `omega(omega)`, which is not in a normal form, and in fact diverges. In a system like SK, and presumably this tree calculus, we can form a similar expression, where the "function part" (i.e. left sub-tree) diverges with no normal form. That's unavoidable, due to the halting problem. I think the claim is that we never need to write such expressions, since there's always an alternative which behaves the same but whose "function part" has a normal form. As a (slightly) more practical example, consider some code like: adjust = (lambda x: x + 1) if increase else (lambda x: x - 1) The function `adjust` is not in a normal form, since it depends on the value of `increase` (when truthy, `adjust` will increment; when falsy it'll decrement). Yet most programmers would probably avoid that, in favour of this: adjust = lambda x: x + 1 if increase else x - 1 Both implementations of `adjust` will behave the same, but the second is in a normal form.
  - calf 2y ago
    I'm rusty but doesn't the increase depend differently, the second adjust lets you decide to assign a value for the variable increase much later, whereas the first adjust fixes the value of increase at the point of evaluating that very assignment statement. There's a name for this, dynamic scoping or something.
    - smsm42 2y ago
      Yes, the two are not identical - in the former, increase is not the part of the closure, in the latter it is. Test: increase = True adjust1 = (lambda x: x + 1) if increase else (lambda x: x - 1) adjust2 = lambda x: x + 1 if increase else x - 1 print(adjust1(42)) print(adjust2(42)) increase = False print(adjust1(42)) print(adjust2(42))

__MatrixMan__ 2y ago

Thanks for the links, I'll be reading up on these. When I signed up for a computer science degree, I was hoping I'd learn this stuff (if not this calculus, than enough context to grapple with it at least). What I actually got was software engineering. Snore.

calf 2y ago
The Theoretical Programming Languages class I took for my minor at Princeton was okay, basically they just taught from Benjamin Pierce's textbook. I'm sure there are other undergrad level intro class syllabi available if that's something you have spare time to self study.