Combinatory Logic (2020) | Hacker News Reader

Combinatory Logic (2020)

plato.stanford.edu

119 pointsnz21 comments

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

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).

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?

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.

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

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.

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

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

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).

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.

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.

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.

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.

I don't think its useful to refer to every symbolic structure that people employ to build machines as "math." There is more to Facebook and Midjourney than the equations used to represent their operation.

Computers compute — they’re a replacement for people doing arithmetic on paper forms.

Fundamentally, there’s a mathematical representation of their computational system.

Also, you admit that equations are driving the core of both systems I described:

- algorithmic manipulation

- SD images

>equations are driving the core of both systems I described

Everything in society uses symbolic representation, but is not driven by symbolic representation, but the people who create those representations.

>unprovable statements

Nonsensical is better in modern discussions than "unprovable". It shows that statements that were previously (and currently by some) thought to be mathematical are actually nonsense just like "x tastes like chicken" but more devious. Asking if a Turing machine with M memory halts in less than N steps is sane and provable.

http://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/e...

> Did Gödel Really Prove That There Exist True yet Unprovable Statements?

> Of course not! All his “statements” were meaningless!

> Every statement that starts : “for every integer n . . .” or “there exists an integer n . . .”, is completely meaningless, since it tacitly assumes that there are infinitely many integers. Of course, there are only finitely many of them, since our worlds, both the physical and the mathematical, are finite.

> The statement “n + n = 2n for every integer n” is meaningless. It is only true for every _finite_ integer. It is also true for symbolic n.

Eehrm? This is not the modern view on math.

In modern math Gödel's theorems are currently regarded as its wiki article talks about it : https://en.wikipedia.org/wiki/Gödel's_incompleteness_theorem... .

You end up with a tower of “universes” that each have some statements they can’t prove which are provable in a higher universe.

You might wonder about the limit… but axioms are only interesting when finite: if you have infinite axioms, just assume the true statements.

You might wonder which those are… but then you’re confronted with the fact it’s all made up and you can have consistent systems from contrary axioms, eg either allowing or disallowing choice.

Mathematics is useful because it gives us a language to tell stories where we can accurately guess questions like “what came before?” or “what happens next?” and where we can describe similarities between stories.

A modern ontology.

Reply on news.ycombinator.com