Search This Blog

14 June 2015

the Promised PizzaQ Hint / The Thing / now with Pretty Colors! / Hint to the Clueless, by Moshe ben Maimon / al-Saladin takes 2 Ibuprofen and calls Maimonides in the morning


Cliquez pour le plus grande
توسيع
כדי להגדיל

Vleeptron promised to maybe, if you're nice and send Bitcoin, offer a HINT to the CLUELESS regarding the most recent wtf? PizzaQ. 

("Hint to the Clueless" is the title of a classic of Jewish wisdom by Moshe ben Maimon, a.k.a. Moses Maimonides, physician to al-Saladin.)

Our Mensch-on-the-Ground in Helvetia solved this PizzaQ, but will not tell us How, and says he doesn't want our lousy Pizza. So the Pizza is still available for the first Correct Solution.

The 2 Things above are The Same Thing. The Left Thing has pretty colors, and some capital letters and positive non-zero integers. And 2 arrows.

As the Helvetian Mensch indicated, these images of The Thing were obtained by a New Scientific Technique never previously used to examine These Kinds of Things. Without the work of these Boffins, Vleeptron would have No Thing to show the blogosphere. The previous Best Image of This Kind of Thing was like the image of a polar bear in an Arctic blizzard, or a black cat in a coal bin.

So now you know Everything There Is to Know about The Thing, so giving it its Name and its Locus should be a Walk In The Park. The Pizza is practically in your mouth.

You can do this. You're smart.

Alternatively, if you can't do this, you're Not Smart.

10 June 2015

long-forbidden boyhood candy / Makes you look Cool! / Just like Dad! No Lighter Required!


Click to enlarge.

My new niece from Chile is fond of chewing gum packaged to resemble a cigarette pack. She rolls the pack into her t-shirt sleeve.

We enjoyed the above Forbidden Candy as boys. The manufacturers had long-term deals with the cigarette manufacturers, and the candy cigarette brands were the most famous cigarette brands. (I liked Lucky Strike cig candy.)

Ciudad Vleeptron UnderWay map.

06 June 2015

ATTENTION tout lovers of Church & Kleene Lambda Calculus / wish my French were good enough / I'd tell you so much more / Darling je vous aime beaucoups ... if you want to feel real nice / ask M. le docteur de rock n roll pour advice ... / Iles des Sourds / cliquez ici pour The Zombies

Cliquez les fiches pour le plus grande.

the strangest e-list I belong to
(since U.N.C.L.E. shut down Silk Road) is Coq-Club, a c-Space meeting locus for the world's lovers of theorem proving assistants and the Lambda calculus of Church and Kleen. You know who you are. You might be a Dutch Power Cow (cf. Vleeptron Link List).

Cette homme posted to Coq-Club that he was a newbie, so he asked if he could only post in English.

I am hoping I can pump Laurent for stuff I need. I sent him the above Donald Evans faux stamps. I think that's fair. Unexpected Surprise Eyeball Beauty from an imaginary French-speaking archipelago!


Suis romanceur btw. That's my day job.

======================
 

If you know anything about Python, or own a Python, or lots of Pythons (Florida has a gazillion giant unwanted Burmese pythons that eat pet dogs and small humans), SVP Leave A Comment. I have Python issues and I need help.

I know a woman whose pet constrictor trapped her in her kitchen, kept her just out of reach of the phone, and spent an hour swallowing her before she managed to get help. He had devoured most of her left arm and wanted more. I don't know what we taste like, but those Ecuadorian rugby lads do. Polar bears like to hunt and kill us, but they don't like the way we taste, so they sniff us and then walk off without eating us. I hate when fresh-killed protein goes to waste like that.

===========

salut Laurent Fournier --
Suis anglophone de USA. I have been on Coq-Club for 4 years. All posts have been en anglais, jamais français.
I do not know if this is a Rule or Law of Coq-Club, or only a generally observed convention.
Bob
Massachusetts USA
P.S. Do you like Python? Did you use BASIC (or dialect of BASIC) before Python?
----- Original Message -----
Sent: Thursday, May 21, 2015 5:26 AM
Subject: [Coq-Club] Newbies Question

Hello everyone,
I’m new on this mailing list…I do not know if posts can be in French or should be in English !

My concern is about the following Python code (can be translated in any language !)
________________________________________________
def value(d, f, i, p, k, x):
    assert d>0 and f>=d and x>=0 and x<=100 and i>0 and p>=0 and k>=0 #PRECOND
    if i == 1: return d, 1
    r, s = p if k==i-1 else p-1, 1 if p==1 else 0
    u, v = (i-1)*(p-1)+k+s, (i-1)*(p-1)+k+r
    if v > f: v = f
    t = ((100-x)*u+x*v)//100
    q = (t-1)//i
    return 1+q, t-i*q

def simu(d, f, x):
    print ('init:%d final:%d speed:%d' % (d, f, x))
    po, ko, to = d, 0, 0
    for i in range(1, f+10):
        p, k = value(d, f, i, po, ko, x)
        t, po, ko = k*p +(i-k)*(p-1), p, k
        assert p>0 and k>0                  #POST0
        if p == po: assert k<=ko         #POST1
        else: assert p=to #POST2
        to = t
        print ('%d: %d*%d+%d*%d=%d' % (i, k, p, i-k, p-1, t))

if __name__ == '__main__':
    for j in range (1, 200): # for instance !
        for s in range(101):
            simu(d=j, f=679, x=s)

A simple simulation shows that the assertions in POST0,1,2 never raise, but I need a FORMAL PROOF that I can remove those 3 lines and be sure that the post-conditions will always be verified. (All parameters are integers and // means “integer division”)

I also need to put the proof in a LaTeX formatted paper if not too long.

Question: Is COQ the right tool to get this proof ?
(consider I do not know COQ and do not expect to spend 2 years in training for that)
If the answer is YES, which lab could be able to do the job (get the proof) ?

Merci d’avance pour votre aide,

Laurent Fournier, PhD.
============


salut Laurent Fournier --
Finally ... my first Coq-Club e-mail pas en anglais!
----- Original Message -----
Sent: Saturday, June 06, 2015 7:58 AM
Subject: Re: [Coq-Club] Partial application is not allowed while using Function

Olá Marcus,

Acabei de ver a tua mensagem! Se quiseres eu posso tentar ajudar-te… consegues dar-me mais algum context (por exemplo o ficheiro em que ela falha)? Se quiseres manda-me o ficheiro e eu tento ajudar-te aqui…

Um alternativa pode ser usares of Program Fixpoint (embora este seja melhor para raciocinar sobre funções com tipos dependentes).

Diz coisas ;-)

Um abraço,
David
I have never had to "work" to be fluent in English, my head was born with English.
When I can't get to Europe, I drive a half-day north to Montreal to stretch my francais. They all understand my fine, expensive ecole Parisienne because most of their movies and TV and music are Parisienne.
But Parisiennes can't understand a thing Quebecers say, it's like Finno-Ugric to Parisiennes.
What communication I've managed in other languages, I thank my Latin class. The Romans taught EVERYONE (and killed them if they didn't speak Latin right ... Miss Murphy only gave me bad grades and Dirty Looks).
But next vie I will choose a language I can use to talk to the Living rather than aux les Mortes.
* * *
SVP if you can spare a little time to help a pathetic and perdu amateur ...
Tell me your thoughts about Python. How did you get to Python?
I have Python on my ordinateur, but I have barely touched it.
Should I invest heavily in learning Python? Or should I find a better HLL language for my programming needs?
Any help you can offer, any tips ... at this moment my beloved ability to code has been Shut Off, and I need a new platform to get back to coding.
Bob le Potzer du Coq
Massachusetts USA
PS: Ton "saintexupery" est Antoine de? Have you read "Vol de Nuit"?
====================