Stories that I cooked up or found online that are of potential use in explaining PL concepts.
In the cafeteria, often the size/quantity of food served would be less than what we are paying for.
To whom is the blame assigned in effect? No-one. Everyone gets scot-free.
Proven by infinite loop!
—
Guy1: Who are you?
Guy2: (Gesturing to the one beside him) I'm his friend.
Guy1: Who is he?
Guy2: He's my friend.
You don't get an answer. It's a loop. Still it looks sound.
—
Here's another one:
Fixpoint absurdity : False := absurdity.
absurdity is kind of appealing to itself to say that it's correct.
Of course, coq doesn't allow this.
| Stage | Analogy |
|---|---|
| Type | A promise to do something |
| Implementation | What's actually done |
| Type-checking | See if the promise was kept |
Mother (opening the refridgerator): Oh, we are running low on milk.
Mother (to her son): Go to the store for me, would you?
Son understands that his mother means for him to go to the grocery shop and buy a few packets of milk. That's because he is a human.
If the son was a machine was a machine name SON instead of a human, it could've been interpreted differently.
SON could've
Go to the grocery store, buy 2 packets of milk, come back home and put the milk packets in the refridgerator.
The level of detail depends on the guarantees that we want.
Even at this point, nothing stops SON from taking the milk back out from the refridgerator right after keeping it inside (and thus fulfilling the contract).
—
Within a reasonable amount of time.
But what is reasonable?
—
An example:
Python string formatting mini-language is given by a sort of grammar: https://docs.python.org/3/library/string.html#formatspec
format_spec ::= [[fill]align][sign]["z"]["#"]["0"][width][grouping_option]["." precision][type]
fill ::= <any character>
align ::= "<" | ">" | "=" | "^"
sign ::= "+" | "-" | " "
width ::= digit+
grouping_option ::= "_" | ","
precision ::= digit+
type ::= "b" | "c" | "d" | "e" | "E" | "f" | "F" | "g" | "G" | "n" | "o" | "s" | "x" | "X" | "%"
But there's more to it.
If we follow this grammar, we can have
.precision d
which isn't actually possible in Python because precision cannot be used if type is int.
In natural languages.
It's here.
is like
λ 'it. λ 'here. => 'it is 'here
Consider a speaker is faced with a question that he finds difficult to answer. He tell the person who asked the question that he'll answer the question once he finishes the talk.
noanswer U talkover
Suppose the speaker managed his talk such that he finished his talk with no time for question.
Under weak until, the promise is upheld. But not for strong until.
Two inverted bowls: A and B We are told that there is a marble underneath one of them: A ∨ B From this can we tell which bowl has the marble?
No.
That's where constructive logic differs from classical logic.
My friend and I are drinking tea. I finished my cup. Friend is still drinking. To keep him company, I refill my glass. He finished, but now I'm still drinking, so he refills as well. This goes on.
How many times should I refill my glass till we can both finish our cups at the same time?
Another scenario: There are only ₹101 and ₹11 currency notes. I need to pay exactly ₹100 to my friend. He can return money as well. Is it possible to pay the ₹100 with just ₹101 and ₹11 notes?
Apparently a sign at a diner:
Kids eat free
No minors allowed
(Got this thought from the wikipedia page for the Eragon books.)