(no subject)

Иногда мне бывает настолько лень мыть вилки, что я ем зубочистками. Я знаю как получились китайские палочки.

* * *
Внезапно узал, что под словом «сыроедение» обычно подразумевают веганское/вегетарианское сыроедение. Фу, пустышка.
Я-то думал, в качестве сыроедеения прокатит тартар с лучком, помидоркой да редиской, метт, карпаччо, крудо, севиче, строганина, сашими, икра и прочие, прочие нежно любимые мною вкусности.

* * *
tiani_tolkay писала, что люди, питающиеся исключительно “пустой пищей” вызывают у неё отторжение. Сперва признаюсь, что ничего не имею время от времени против колбаски с белым хлебом, особенно если ещё с хреном вкусным.

tiani_tolkay говорила только о людях, которые едят _исключительно_ “пустую пищу”, но тем не менее, очень хочется выступить в защиту и людей, которые только время от времени питаются чем попало. Т.е. в защиту себя в том числе. :-)
Нет, вкусно поесть время от времени прекрасно. Сегодня вот вечер пятницы, хоть я и воздержался от вина, стейк себе всё-таки сделал. Отменный, нежирный стейк с розовинкой внутри. С зеленью.
Но это раз или два в неделю!

А вот голод или голоднная слабость/головокружение, что посреди работы или другого затягивающего дела, это исключительно неудобное обстоятельство. И к необходимости отвлечься и что-нибудь съесть (при этом постаравшись не потерять нить работы) я отношусь с не большим энтузиазмом, чем, извините, к обратному процессу. Чисто потребность организма, никакой эстетики. И на обед я с удовольствием хомячу полуфабрикат из ближайшей Эдеки по евро килограмм. Жиры, белки, углеводы в нормальном соотношении, калорий в самый раз, а главное — сунул в микроволновку и готово. Весь обед вместе с “приготовлением” 10-15 минут от “встал из-за компа” до “вернулся, вспомнил что делал и приступил к работе”.
Через час я уже не вспомню, был ли это Kartoffelauflauf, Gemüselasagne или крем-суп какой, я в любом случае пока ел думал о причиах странной рассинхронизации базы облачной данных, а не о вкусе еды, вкуса еды я вообще не заметил. Для вкуса у меня ужин, а обед посреди работы — чтобы утолить потребность организма в энергии, причём так чтобы от этого не страдал пищеварительный тракт, туды его в качель. (Если бы ему было всё равно, я бы обедал таблеткой глюкозы и белково-витаминным коктейлем.)

(no subject)

Фух. Осилил все статьи товарища codedot'а. Единственное, хорошо-б в “Interaction Nets in Russian” добавить раздел про направленные комбинаторы и их пользу для народного хозяйства.

(no subject)

Introduction

We regard theory as a conglomerate of a language for writing statements, a language for writing valid proofs and a collection of axioms (basis of statements the theory assumes to be true). A theory is said to be consistent if there is no pair of valid proofs proving contradictory statements. A theory is said to be capable of reflection iff it's possible to write the statement "this theory is consistent" in the language of the theory itself.

There are three main results concerning consistency:
1) (Gödel's Second Incompleteness Theorem) All common non-trivial theories cannot prove their own consistency. This applies essentially to all theories that include the notion of an infinite ordered set with a distinguished zero object (e. g. natural numbers) and provide a way to construct a larger object for any given one.

2) (Gentzen's Algorithm) For common theories there is an algorithm that "analytically verifies" their proofs. Analytically checked proofs can be directly shown to be contradiction-free. This does not contradict to the (1) because no theory which is subject to (1) can internally show that verification algorithm holds for every valid input.

3) (Dan Willard's Self-verifying theories) There are non-trivial exceptions to (1). They are not only capable of reflection, but even prove their own consistency.

The theories (3) share a common property: their proofs can be analytically verified inplace. Whereas for theories which Gödel's Theorem (1) applies the algorithm normally requires enormous amounts of additional working space. This goes so far that analytical verification of some proofs could be fundamentally physically infeasible due to finiteness of the visible universe.

This could be a clue to understanding the Gödel's Theorem (1): maybe the true reason we cannot show Gentzent's algorithm to succeed always without additional assumptions exactly because it doesn't phyiscally do so.

In this case we could use a physical estimate for information content of the visible universe and restrict our attention to proofs of the "modest" length which are at least in theory verifiable. Then we'd be pretty sure that these proofs are definitely noncontradictous. If it would turn out that upper bound on proof length is beyond that of normal human-developed proofs, a longstanding question about solidity of mathematical foundations would be at least partially solved.

Now how can we find the upper bound for proof length starting with informational content of the universe? It appears that the following approach could roughly do.

The Programme

( Read more... )