Здорово! Удачи! Очень полезное дело.

славно, обязательно будем почитать :)

обязательно! и хочется и вторую книгу тоже - advanced types & pl

(Reply to this) (Thread)

Вторая она скорее сборник статей, не думаю что она будет большой популярностью пользоваться.

(Reply to this) (Parent)

а есть CVS/svn с исходниками, чтобы вычитывать актуальное и генерировать diff'ы? может быть стоит где-нить на code.google.com сделать рассылку и там же bugtracker? мы такое делали с Introduction to Functional Programming

(Reply to this) (Thread)

Пока что нет, но сделать что-то подобное, конечно, надо.

(Reply to this) (Parent) (Thread)

пожалуйста, напиши - я с удовольствием подключусь к переводу такой замечательной книги

(Reply to this) (Parent) (Thread)

Ты хочешь участвовать в переводе самого текста? Было бы здорово.

(Reply to this) (Parent) (Thread)

да, по мере возможностей мог бы переводить - у меня сейчас работа "не бей лежачего" и времени много :-)
я поэтому про репозиторий и спрашивал - какой-нибудь меркуриал, гит или еще что-то

(Reply to this) (Parent)

Мы как-то тоже делали cловарь терминов, правда там цель была не столько для перевода, сколько для выработки терминов для общения.

(Reply to this) (Thread)

Спасибо, хороший словарик.
Может быть, мне просто попробовать в него влиться?

(Reply to this) (Parent) (Thread)

конечно, было бы здорово!

Из замеченного в списке терминов (не претендую на правильность):

bounded quantification

ограниченная квантификация (в списке на сайте пропущена буква, наверняка опечатка, но на всякий случай, чтоб копи-пастом не разошлось)

featherweight Java

облегчённая Java (я не в курсе о чём речь, но может „легковесная“; хотя далее есть “lightweight formal method” и там уж точно „облегчённый” лучше)

simply typed lambda calculus

простое типизированное просто-типизированное лямбда-исчисление (simple vs. simply, наречие относится к “typed”, а не к “λ calculus”)

termination proof

доказательство гарантии завершения (присутствие сразу и слова „доказательство”, и „гарантии” мне кажется излишним. Может выкинуть „гарантии” (и, возможно, заменить „завершения” на „завершимости”)?)

trapped run-time error

диагностируемая ошибка времени выполнения (тут видимо нужен контекст, но меня смущает несоответствие “trapped” (прилагательное, от глагола прошедшего времени) и „диагностируемая” (прилагательное, от инфинитива (? — я не спец в русском). Я бы перевёл как „перехваченная/обнаруженная ошибка времени выполнения”.)

logical framework

логическая конструкция (вспоминая лекции по матану, там про подобные по смыслу вещи говорилось „аппарат”, соответственно „логический аппарат”)

well founded

вполне обоснованный („хорошо обоснованный”? нужен контекст)

(Reply to this) (Parent) (Thread)

Спасибо!
Вообще говоря, такое обсуждение, наверное, лучше уже в список рассылки. Поскольку Вас там пока нет, отвечаю здесь.

featherweight Java

Это название игрушечного языка программирования, который описывается в одной из глав (разумеется, основанного на Java). Мне кажется, "легковесная" в названии звучит неестественно.

simply typed lambda calculus

Формально Вы правы, но "просто-типизированное" через дефис уж больно громоздко по-русски. Поскольку из типизированных лямбда-исчислений это и вправду простейшее, а все остальные являются его расширениями, термин, хоть и не является точным переводом, в заблуждение не вводит.

termination proof

А вот здесь я, наоборот, буду защищать громоздкий вариант в угоду точности. "Доказательство завершения" -- это доказательство, что _конкретное_ вычисление завершается. "Доказательство завершимости" -- доказательство, что (может быть, и всякое) вычисоление _способно_ завершиться, то есть, _возможно_, завершается. Более короткого выражения, которое бы указывало, что _всякое_ вычисление _всегда_ завершается, я не нашел.

trapped run-time error

trapped здесь просто пассивное причастие, без привязки ко времени, и смысл выражения -- a type of error that is always being trapped.

logical framework

Вот здесь Вы, может быть, правы. Надо посмотреть, насколько хорошо "аппарат" ложится в текст (а также посмотреть во втором томе, где про этот самый Edinburgh framework подробнее рассказывается, насколько подходит по смыслу.

well founded

Это термин, который, безусловно, существует в русскоязычной логической литературе. Я попытался поискать по словарям и Википедии, а также вспомнить, как именно мне когда-то это понятие называл русский лектор, и, вроде бы, well ordering переводится как "полный порядок", а well-ordered set как "вполне упорядоченное множество". Но хотелось бы, чтобы какой-нибудь активно практикующий логик это подтвердил.

Сейчас я перегоню терминологию в ваш словарь, и, надеюсь, больше народу посмотрит и выскажет свое мнение.

(Reply to this) (Parent) (Thread)

Имеет тогда смысл после обновления нашего словаря кинуть объявление на гугл-группы SPbHUG и MskHUG, чтоб народ посмотрел, ну и заодно туда можно приглашение кинуть, так охват довольно большой получится.

(Reply to this) (Parent)

а ты там вики сделать не хочешь? было бы удобно.

(Reply to this) (Thread)

ОГО, только вроде уехал, а уже такую кучу напереводил!

(Reply to this) (Parent) (Thread)

Переводил, разумеется, раньше. Сейчас просто получил сигнал, что договор заключен, и можно выходить на публику.

(Reply to this) (Parent)

Я не очень понимаю, зачем wiki. Мне, по крайней мере пока, хотелось бы иметь решающее слово при редактировании текста. А для дискуссии и рассылка ничуть не хуже.

(Reply to this) (Parent)

ну вот на code.google.com и вики есть - по крайней мере для перевода терминов, это очень удобно

(Reply to this) (Parent)

А кто издавать будет?

(Reply to this) (Thread)

Не знаю. Этим занимается zelych@lj.

(Reply to this) (Parent)

Я могу вам по почте рассказать в подробностях (jorpic на гмейле).
Если вы имеете отношение к издательству МЦНМО, то можно заодно обсудить варианты сотрудничества (я думаю, для книжки это будет полезно).

(Reply to this) (Parent)

отлично, поможем обязательно!

а вы могли бы как-нибудь помочь издать http://code.google.com/p/funprog-ru/ по завершению?, небольшим тиражом .. у нас походу завязок на издательства не особо :(

там у нас тоже есть список терминов, если интересно - http://code.google.com/p/funprog-ru/wiki/TermsTranslation

(Reply to this) (Thread)

У меня у самого тоже с издательствами контактов особых нет. Попробуйте поговорить с zelych@lj или mccme@lj.

(Reply to this) (Parent)

с днем рожденья!

(Reply to this) (Thread)

Спасибо!

(Reply to this) (Parent)

С днём рождения, кстати.

(Reply to this) (Thread)

Спасибо!

(Reply to this) (Parent)

Начал читать. Может потому что вечер, но на данной фразе стек в мозгу явно переполнился...

Книга сосредоточена на использовании
систем типов в языках программирования, за счет некоторых тем (например,
денотационной семантики), которые, вероятно, были бы включены в более ма-
тематически ориентированный текст по типизированным лямбда-исчислениям.

(Reply to this) (Thread)

The book concentrates on the use of type systems in programming languages, at the expense of some topics (such as denotational semantics) that probably would be included in a more mathematical on typed lambda-calculi.

Русский перевод тяжеловеснее, согласен. Варианты?

(Reply to this) (Parent)