<KipIngram>
So I'm starting to get at least a few of the lambda calculus quiz problems right.
<KipIngram>
I haven't quite gotten it pat for some of the "orderings" of things.
boru` has joined #forth
boru has quit [Disconnected by services]
boru` is now known as boru
sts-q has quit [Ping timeout: 276 seconds]
sts-q has joined #forth
dave0 has joined #forth
<dave0>
maw
jedb_ has joined #forth
jedb has quit [Ping timeout: 252 seconds]
jedb_ is now known as jedb
andrei-n has joined #forth
Kumool has quit [Ping timeout: 268 seconds]
Kumool has joined #forth
gravicappa has joined #forth
gravicappa has quit [Ping timeout: 260 seconds]
gravicappa has joined #forth
gravicappa has quit [Ping timeout: 252 seconds]
gravicappa has joined #forth
<DKordic>
How do I add Content to Amazon Web S***r!? Do I need iOS or can it be done with Android!?
spoofer_ has quit [Read error: Connection reset by peer]
spoofer has joined #forth
jedb has quit [Quit: Leaving]
jedb has joined #forth
pointfree has joined #forth
<DKordic>
Q: Combinators?! How to most convenniently construct and apply Combinators?! W/Funarg_problem ?!
<DKordic>
Combinators are at the essence of both Lisp, >>apply<<, and Forth, >>compose<<. Or even better let Us call it <<Forth>> rather thann <compose>>.
<DKordic>
Challenge: >> [ dfn ( fix M ) ( M ( fix M ) ) ] << or the Turing's Construction >> [ dfn fix ( A A ) ( A T M ) ( M ( T T M ) ) ] <<!
<DKordic>
An example of my solution (so far): >> [ dfn ( apply M A ) ( M A ) ( Forth M1 M2 A ) ( M2 ( M1 A ) ) ] <<.
<DKordic>
KipIngram: What do You think?
tech_exorcist has joined #forth
dave0 has quit [Quit: dave's not here]
<siraben>
remexre: yay, was able to prove a compiler to a stack machine correct wrt. a small-step operational semantics
<siraben>
since the programs always terminate, I didn't use bisimulation or anything
<siraben>
`forall (e : aexp) (st : state) (s : stack) (p : prog), stack_multistep st (s_compile e ++ p, s) (p, aeval st e :: s).`
<siraben>
where stack_multistep is the reflexive transitive closure of the small-step rules of the stack machine
<siraben>
later on I'll try a compiler for IMP to a stack machine with jumps, that should be sufficiently complex
f-a has joined #forth
f-a has quit [Ping timeout: 240 seconds]
f-a has joined #forth
f-a has quit [Read error: Connection reset by peer]
f-a has joined #forth
f-a has quit [Ping timeout: 240 seconds]
f-a has joined #forth
<remexre>
siraben: is that from PLF? I remember Adam Chlipala's book had something similar at the start too (though that one ramps up hard + fast iirc...)
xek_ is now known as xek
f-a has quit [Quit: leaving]
pointfree has quit [Quit: Connection closed for inactivity]
<KipIngram>
DKordic - I'm afraid I don't immediately follow all that yet.
f-a has joined #forth
f-a_ has joined #forth
f-a has quit [Read error: Connection reset by peer]
f-a_ has quit [Client Quit]
f-a has joined #forth
f-a has quit [Ping timeout: 265 seconds]
<siraben>
remexre: yeah from PLF
<siraben>
Chlipala's book goes really fast, one already needs to be a competent user before reading it for sure
<remexre>
yeah, it was actually my first coq book... picked it up at MIT bookstore when on vacation to boston because the idea of formally verifying programs sounded neat
<remexre>
then got immediately lost and didn't come back to it for years, lol
<KipIngram>
So, formally verifying code IS neat. But whatever we humans do when we look at, for instance, a Forth definition, is also neat. We somehow hold it in our minds, and "see" its correctness. We're human, so that is an imperfect process. We can err. But it's still fascinating that our minds can do that. What exactly do you suppose it is we're doing?
<KipIngram>
Related - the mere fact that we believe in the correctness of Gödel's Theorem means that we can somehow perceive truth even where it can't be proven.
<KipIngram>
What exactly are we perceiving? It just smacks to me of an indication that something non-algorithmic is happening in our minds.
<KipIngram>
I mean, if you want to think in a very pure way, then PROVING truth should be the only way to DEFINE truth. But it's not - we can transcend that somehow.
<KipIngram>
It's fascinating.
<f-a>
but it is not, isn’t it?
<KipIngram>
Didn't follow - not what?
<f-a>
first because there has to be some premise X to prove Y
<KipIngram>
Yeah - a system of logic has to have a starting point.
<KipIngram>
Oh gosh - what is that book. Early 20th century...
<KipIngram>
Hang on - I have it here on the coffee table.
<f-a>
don’t spill!
<KipIngram>
Science and Hypothesis, by Poincare.
<KipIngram>
He contends that everything is a tautology.
<KipIngram>
That the conclusions of a logical analysis are really just a restatement of the postulates.
<KipIngram>
And that's hard to argue with.
<KipIngram>
I.e., the postulates contain all the knowledge to start with.
<KipIngram>
So we never add any new knowledge - not REALLY.
<f-a>
ohhh poincaré
<f-a>
I mostly read him about interpretations of Probability
<f-a>
welp, my grammar is degrading
<KipIngram>
One could argue that all of the knowledge, and all of its practical application, is there in the postulates, but aspects of it are not easy to reach. By logic we bring more facets of it into reach.
<KipIngram>
But it's all "out there" from the jump
<MrMobius>
heh, that type of nonsense someone wrote to get a diessertation is why I ran screaming from philosophy
<KipIngram>
Indeed, indeed.
<KipIngram>
Scientific philosophy is ok in my book, but there are just times to set it aside, that's for sure.
<KipIngram>
"Shut up and calculate" has value as well.
<MrMobius>
I read a book once where the guy said the only way to know truth is to test hypotheses but testing hypotheses reveals other hypotheses you couldn't have known about. Therefore, the pursuit of truth actually drives you farther away from it
<MrMobius>
obviously horseshit but that doesn't stop people from stringing together similar statements that happen to be grammatically correct
<f-a>
was it fayerabend?
<f-a>
he had a point
<KipIngram>
Well, let's put it this way. In the 1700's we couldn't build computers. In the 2000's we can. Obviously something has been accomplished.
<KipIngram>
The same with cars, and microwaves, and cell phones.
<KipIngram>
The pragmatic evidence of the value of scientific reasoning is all around us.
<f-a>
now then
<MrMobius>
i check out when the words people put together stop having anything to do with reality. you are then wasting my time at that point. once philosophy hits that point we're just inventing things that can be said without regard for reality
<f-a>
for the real tought questin
<f-a>
why is youtube/reddit harassing me with liquid meal replacement?
<f-a>
I do not want them
<f-a>
MrMobius: some kind of speculative analysis can be for good
<KipIngram>
lmao...
<KipIngram>
You did SOMETHING to cause that.
<KipIngram>
Who knows what, though...
<f-a>
yeah that is the scary part
<MrMobius>
f-a, but this is not speculation. making claims about reality because you put words together in some way that no longer resembles anything real then leaving fantasy land to inflict your construction on everyone is not speculation
<MrMobius>
no problem with speculating as long as you remain humble
<f-a>
haha
Zarutian_HTC has joined #forth
<KipIngram>
I engage in that kind of thinking from time to time. Mostly involving quantum stuff.
<KipIngram>
Most of the pop-sci coverage of quantum theory is New Age woo.
<KipIngram>
They deliberately cultivate a sense of mysticism around the stuff.
<KipIngram>
There's certainly some weird shit going on in there, but it's not as weird as they make it sound.
<MrMobius>
haha, ya there is
<KipIngram>
I think the "weird" is mostly related to the fact that two separate points in space can be "connected" in a way that breaks our sense of "distance" and "separation."
<MrMobius>
quantum entanglement and we don't understand, therefore out souls are connect - believe my religion
<MrMobius>
*our souls are connected
<KipIngram>
Our intuition tells us that if A and B are at different places, then the only way for them to affect one another is for an effect to be conveyed over space.
<KipIngram>
But that's just not true - A and B can be in different places and yet behave (in some ways) as though they're right by one another.
<KipIngram>
That's weird.
<KipIngram>
But if you just accept that somehow our concept of spacetime misses something, then there isn't any "more weird" after that.
<KipIngram>
And yeah - minds, souls, whatever you want to call them. How does THAT work??? We have no idea.
<KipIngram>
I do NOT believe that our minds are just programs running on our brains. There's something more to it than that.
<KipIngram>
I don't think science is even close to being able to talk about it, though.
<nihilazo>
welcome to the realm of philosophy :D
<KipIngram>
Obviously there is a strong correlation between our thinking / feeling and activity in our brains. I just don't think the one IS the other, with nothing else involved.
<nihilazo>
a world where we all know that there is never going to be a single correct answer but we try and figure it out anyway
<KipIngram>
^^ Indeed.
<KipIngram>
Anyway, back to earlier discussion. DKordic - the thing you asked me my opinion of. Were you specifically asking me about the code-like stuff you'd just written? That you described as your latest thinking?
<KipIngram>
Was that somehow an implemetation of a Forth-like thingie?
<KipIngram>
God, I sound like my sister-in-law. "Thingie." :-|
f-a has left #forth [#forth]
<cmtptr>
cray cray
Zarutian_HTC has quit [Remote host closed the connection]
<KipIngram>
That also sounds like my sister-in-law. :-)
<KipIngram>
I have fun at her expense, but she hasn't turned out to be nearly as flaky as I thought she might when I first met her.
<KipIngram>
Actually has a very responsible job with Southwest Airlines and everything - the kid's done good.
andrei-n has quit [Quit: Leaving]
gravicappa has quit [Ping timeout: 265 seconds]
dave0 has joined #forth
<dave0>
maw
tech_exorcist has quit [Ping timeout: 268 seconds]