Ponton’s site

Yay, another parser in Haskell! That was a Haskell week, but I’m glad I had an opportunity to recall this beautiful full-of-math language.

This program reads an annotated program — a program with assertions. Assertions are just logic formulas. We use them to describe the program state between instructions, ie. variable x is equal to variable y squared. But assertions cannot be random, they must be derived from Hoare’s logic axioms and rules (which base on the formal semantic of the language). How do we know if there is an derivation of a program?

Here verification condicitions come. They are logic formulas too, but generated from annotated program. If all of them are true, then the program is derivable. More information here: http://www.macs.hw.ac.uk/~air/hic-hisd/ and http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html. The whole point is about formal verification of programs. Nowadays compiler can tell only whether given program has a syntax or type error. It doesn’t know anything about how this program should work and can’t say something like: “This program certainly does not multiply matrices.”. Assertions are some way to tell the programmer’s intentions to the compiler: “This is my piece of code and it should multiply two matrices”, and thus, by generating verification conditions and using automated theorem proving it could say: “It does.”.

So after a boring digression… this program reads an annotated program in a simple imperative language and generates verification conditions. That’s all.

All files are here: http://srednikpe.org/src/vc/

Computer science and math, English computer science, haskell, math, my code

From here.

An engineer, a physicist and a mathematician are staying in a hotel.
The engineer wakes up and smells smoke. He goes out into the hallway and sees a fire, so he fills a trash can from his room with water and douses the fire. He goes back to bed.
Later, the physicist wakes up and smells smoke. He opens his door and sees a fire in the hallway. He walks down the hall to a fire hose and after calculating the flame velocity, distance, water pressure, trajectory, etc. extinguishes the fire with the minimum amount of water and energy needed.
Later, the mathematician wakes up and smells smoke. He goes to the hall, sees the fire and then the fire hose. He thinks for a moment and then exclaims, “Ah, a solution exists!” and then goes back to bed.

Asked if he believes in one God, a mathematician answered:
” Yes, up to isomorphism.”

A mathematician, scientist, and engineer are each asked: “Suppose we define a horse’s tail to be a leg. How many legs does a horse have?” The mathematician answers “5″; the scientist “1″; and the engineer says “But you can’t do that!

One day a farmer called up an engineer, a physicist, and a mathematician and asked them to fence of the largest possible area with the least amount of fence.
The engineer made the fence in a circle and proclaimed that he had the most efficient design.
The physicist made a long, straight line and proclaimed “We can assume the length is infinite…” and pointed out that fencing off half of the Earth was certainly a more efficient way to do it.
The Mathematician just laughed at them. He built a tiny fence around himself and said “I declare myself to be on the outside.”

A mathematician belives nothing until it is proven
A physicist believes everything until it is proven wrong
A chemist doesn’t care
biologist doesn’t understand the question.

Two male mathematicians are in a bar. The first one says to the second that the average person knows very little about basic mathematics. The second one disagrees, and claims that most people can cope with a reasonable amount of math.
The first mathematician goes off to the washroom, and in his absence the second calls over the waitress. He tells her that in a few minutes, after his friend has returned, he will call her over and ask her a question. All she has to do is answer one third x cubed.
She repeats “one thir — dex cue”?
He repeats “one third x cubed”.
Her: `one thir dex cuebd’? Yes, that’s right, he says. So she agrees, and goes off mumbling to herself, “one thir dex cuebd…”.
The first guy returns and the second proposes a bet to prove his point, that most people do know something about basic math. He says he will ask the blonde waitress an integral, and the first laughingly agrees. The second man calls over the waitress and asks “what is the integral of x squared?”.
The waitress says “one third x cubed” and while walking away, turns back and says over her shoulder “plus a constant!”

Computer science and math, English hehe, math

W sobotę po kolokwium (tak, było w sobotę…) czekając na ludzi, zaczepił mnie jakiś student psychologii z prośbą o wypełnienie ankiety. Tematem ankiety była seksualność. Miałem chwilę czasu i byłem ciekawy, o co chodzi (tak, zaciekawiła mnie ta seksualność), więc przystąpiłem do wypełniania.

Budowa ankiety była dosyć prosta. Zawierała jakieś 40-50 pytań tak/nie typu “czy miewasz erotyczne sny z X?”, “czy uprawiałeś seks z X?”, “czy potrafisz być czuły wobec X?”, “czy podniecają Cię ładne/ładni X?”, “czy czujesz potrzebę zrealizowania się w związku z X?”, gdzie pytania o numerach nieparzystych miały zamiast X słowo “dziewczynami”, a reszta ─ “chłopakami”. Nie powiem, jak odpowiadałem, w każdym razie zaznaczyłem niektóre z tych parzystych. :>

Przy okazji wpadłem na pomysł współczynnika durności testu. Większość z nich zawiera potwarzające się pytania, tylko inaczej sformułowane. Ma to na celu wyeliminowanie czegośtam, nieważne. W każdym razie, jeśli jest tego za dużo, to to irytuje.

Teraz zacznie się matematyka. Niech Q będzie zbiorem pytań ankiety, a relacja = określona na zbiorze [tex]Q^2[/tex] jest zdefiniowana następująco:

Jeśli a i b należą do zbioru Q, to a = b [tex]\Longleftrightarrow[/tex] a pyta o to samo, co b.

Oczywistym jest, że = jest relacją równoważności. Napis [a] (dla a należącego do Q) będzie oznaczał klasę abstrakcji względem tej relacji (dla humanistów: zbiór wszystkich pytań pytających o to samo, co a). Współczynnik durności ankiety, S, definiuje wzór:

[tex]S = \frac{|Q|}{| \lbrace [a] | a \in Q \rbrace|}[/tex]

Czyli innymi słowy stosunek liczby pytań do liczby pytań unikalnych. :> Teraz trzeba wymyślić jakąś skalę, ja przyjąłem, że do 1,1 ankieta normalna, do 1,4 jest normalnym psychologicznym testem, a do 2,0 jest durna. Powyżej 2,0 staje się niepoważna.

Computer science and math, Polskie, Przemyślenia hehe, math

Ostatni tydzień był bardzo fajny. Kilka miłych zdarzeń się zbiegło w czasie. Ale już wtedy wiedziałem, że za kilka dni czeka mnie jakaś niemiła niespodzianka. Przecież nie może być zawsze tak cudownie. Życie to sinusoida.

I doczekałem się. Nawet mi to nie zepsuło humoru. Wręcz przeciwnie - nie myliłem się przecież. ;)

Polskie, Przemyślenia, Real life math, narzekanie

Do baru wchodzi nieskończona liczba matematyków. Pierwszy zamawia jeden kufel piwa, drugi pół kufla, trzeci jedną czwartą i tak dalej. Barman kręci głową z dezaprobatą i nalewa im dwa kufle.

Polskie hehe, math