4 ms·

Combinatory Logic (2020)

119 points by nz 3y ago

jph00 3y ago
Combinators are elegantly expressed in array languages, especially J. Here's a great recent paper with details : https://raw.githubusercontent.com/codereport/Content/main/Publications/Combinatory_Logic_and_Combinators_in_Array_Languages.pdf https://raw.githubusercontent.com/codereport/Content/main/Pu...
- rak1507 3y ago
  Unfortunately (as an array language fan) this isn't really true. Certain function composition operators that exist in array languages appear to have similarity with combinators, however array languages are unable to express true lambda calculus style combinatory logic (without just implementing the reduction rules yourself, which defeats the point).
  - throwaway17_17 3y ago
    Can you expand on this some? I am not super familiar with the array-based group of languages, but so was under the impression that implementing S,K, and I combinators was possible. Is it just the restriction of array arguments or is it something else that inhibits the languages?
    - rak1507 3y ago
      Yeah, you can implement them like you could in anything - it varies per language but the lack of true higher order functions (anything except K) and lazy evaluation (all) means that there's not really an 'elegant' way for anything more than 1 term deep. That's not to say that the 'combinators' in array languages are bad, they're very useful and a nice form of function composition that I wish most other languages had, but they're not really a true combinator in the lambda calculus sense. You can't pass the array language 'combinators' to other combinators.
      - martinsmit 3y ago
        BQN[1] has higher order functions. Of the array languages I've used, it's by far my favourite. That said, I mostly solve small problems for fun in them. [1] https://mlochbaum.github.io/BQN/index.html https://mlochbaum.github.io/BQN/index.html
        rak1507 3y ago
        Yeah BQN sort of has higher order functions but it still distinguishes between functions and data, so I don't think it would be that possible/easy to use combinatory logic style combinators. I haven't used BQN much though, so I could be wrong.
kordlessagain 3y ago
[flagged]
DiscourseFan 3y ago
Yeah whenever I read about stuff like this I always feel the attempt to create formally complete logical systems is inherently flawed.
- brutusborn 3y ago
  I have heard of some problems that are unprovable in some systems but provable in stronger systems (like this: https://en.m.wikipedia.org/wiki/Paris–Harrington_theorem https://en.m.wikipedia.org/wiki/Paris–Harrington_theorem). I wonder if it is possible for an AI to eventually try to prove currently unprovable theorems by producing it’s own formal system? I don’t know enough about Godels Theorems or ML to know if this is even possible.
  - sn41 3y ago
    Godel's theorem applies to all systems strong enough to do arithmetic. When we talk about "powerful" systems, it will inevitably have to do arithmetic. One of the unprovable statements of any such formal system will be that "this system is consistent", which is an important property. [Godel's second incompleteness theorem] I feel that AI in general is headed towards the direction of saying that provability is not really important, let's just head in a pragmatic direction.
    - keithalewis 3y ago
      Prior to Euclid people seemed to be concerned with valid arguments. Mathematical proofs are limited to true or false statements. Math is great when modeling physics, but quite lacking when applied to other human endeavours.
      - zmgsabst 3y ago
        Facebook disagrees: Math lets them manipulate your emotions on behalf of advertisers and spy agencies, alike. As does Midjourney: Math lets them turn a loose description into a high quality picture of that scene.
redrobein 3y ago
For anyone looking for a more gentle introduction to logic and combinators, checkout Raymond Smullyan's "To Mock A Mockingbird".

119 points by nz 3y ago

Combinators are elegantly expressed in array languages, especially J. Here's a great recent paper with details : https://raw.githubusercontent.com/codereport/Content/main/Publications/Combinatory_Logic_and_Combinators_in_Array_Languages.pdf https://raw.githubusercontent.com/codereport/Content/main/Pu...

rak1507 3y ago
Unfortunately (as an array language fan) this isn't really true. Certain function composition operators that exist in array languages appear to have similarity with combinators, however array languages are unable to express true lambda calculus style combinatory logic (without just implementing the reduction rules yourself, which defeats the point).
- throwaway17_17 3y ago
  Can you expand on this some? I am not super familiar with the array-based group of languages, but so was under the impression that implementing S,K, and I combinators was possible. Is it just the restriction of array arguments or is it something else that inhibits the languages?
  - rak1507 3y ago
    Yeah, you can implement them like you could in anything - it varies per language but the lack of true higher order functions (anything except K) and lazy evaluation (all) means that there's not really an 'elegant' way for anything more than 1 term deep. That's not to say that the 'combinators' in array languages are bad, they're very useful and a nice form of function composition that I wish most other languages had, but they're not really a true combinator in the lambda calculus sense. You can't pass the array language 'combinators' to other combinators.
    - martinsmit 3y ago
      BQN[1] has higher order functions. Of the array languages I've used, it's by far my favourite. That said, I mostly solve small problems for fun in them. [1] https://mlochbaum.github.io/BQN/index.html https://mlochbaum.github.io/BQN/index.html
      - rak1507 3y ago
        Yeah BQN sort of has higher order functions but it still distinguishes between functions and data, so I don't think it would be that possible/easy to use combinatory logic style combinators. I haven't used BQN much though, so I could be wrong.

kordlessagain 3y ago

[flagged]

DiscourseFan 3y ago

Yeah whenever I read about stuff like this I always feel the attempt to create formally complete logical systems is inherently flawed.

brutusborn 3y ago
I have heard of some problems that are unprovable in some systems but provable in stronger systems (like this: https://en.m.wikipedia.org/wiki/Paris–Harrington_theorem https://en.m.wikipedia.org/wiki/Paris–Harrington_theorem). I wonder if it is possible for an AI to eventually try to prove currently unprovable theorems by producing it’s own formal system? I don’t know enough about Godels Theorems or ML to know if this is even possible.
- sn41 3y ago
  Godel's theorem applies to all systems strong enough to do arithmetic. When we talk about "powerful" systems, it will inevitably have to do arithmetic. One of the unprovable statements of any such formal system will be that "this system is consistent", which is an important property. [Godel's second incompleteness theorem] I feel that AI in general is headed towards the direction of saying that provability is not really important, let's just head in a pragmatic direction.
  - keithalewis 3y ago
    Prior to Euclid people seemed to be concerned with valid arguments. Mathematical proofs are limited to true or false statements. Math is great when modeling physics, but quite lacking when applied to other human endeavours.
    - zmgsabst 3y ago
      Facebook disagrees: Math lets them manipulate your emotions on behalf of advertisers and spy agencies, alike. As does Midjourney: Math lets them turn a loose description into a high quality picture of that scene.

redrobein 3y ago

For anyone looking for a more gentle introduction to logic and combinators, checkout Raymond Smullyan's "To Mock A Mockingbird".