Алгоритм-самоописувач

[Campana]

Концептуальне питання: чи може існувати програма, яка при запуску або при передачі їй якихось даних видасть на вивід свій код або джерельний текст?

Або загальніше: чи може існувати алгоритм, який на виході дасть свій власний опис?

[Насправді, мене цікавить більш загальна ситуація: чи може функція бути власним значенням. Але оскільки тут не математики зібралися...]

[raven]

man λ-calculus

[Михайло Даниленко]

[isbear:~] ./dmp.pl
Hello, World! I am born!
It's me:
--- !!perl/code: >-
{
    print "Hello, World! I am born!\n";
    my $dump = Dump(\&a);
    print "It's me:\n$dump\n";
}

[isbear:~] cat dmp.pl
#! /usr/bin/perl

use YAML::Syck;
$YAML::Syck::DumpCode = 1;

sub a {
        print "Hello, World! I am born!\n";
        my $dump = Dump ( \&a );
        print "It's me:\n$dump\n";
}

a();

# The End.

Так піде?

[raven]

use YAML::Syck;

Чітер=)

[Михайло Даниленко]

А, ну сорі

[isbear:~] dpkg -L libyaml-perl
/.
/usr
/usr/share
/usr/share/perl5
/usr/share/perl5/YAML
/usr/share/perl5/YAML/Error.pm
/usr/share/perl5/YAML/Loader.pm
/usr/share/perl5/YAML/Dumper.pm
/usr/share/perl5/YAML/Base.pm
/usr/share/perl5/YAML/Tag.pm
/usr/share/perl5/YAML/Loader
/usr/share/perl5/YAML/Loader/Base.pm
/usr/share/perl5/YAML/Marshall.pm
/usr/share/perl5/YAML/Node.pm
/usr/share/perl5/YAML/Dumper
/usr/share/perl5/YAML/Dumper/Base.pm
/usr/share/perl5/YAML/Types.pm
/usr/share/perl5/Test
/usr/share/perl5/Test/YAML.pm
/usr/share/perl5/YAML.pm
/usr/share/man
/usr/share/man/man3
/usr/share/man/man3/YAML::Base.3pm.gz
/usr/share/man/man3/YAML::Loader.3pm.gz
/usr/share/man/man3/Test::YAML.3pm.gz
/usr/share/man/man3/YAML::Node.3pm.gz
/usr/share/man/man3/YAML.3pm.gz
/usr/share/man/man3/YAML::Types.3pm.gz
/usr/share/man/man3/YAML::Tag.3pm.gz
/usr/share/man/man3/YAML::Loader::Base.3pm.gz
/usr/share/man/man3/YAML::Error.3pm.gz
/usr/share/man/man3/YAML::Dumper::Base.3pm.gz
/usr/share/man/man3/YAML::Marshall.3pm.gz
/usr/share/man/man3/YAML::Dumper.3pm.gz
/usr/share/man/man1
/usr/share/man/man1/ysh.1p.gz
/usr/share/doc
/usr/share/doc/libyaml-perl
/usr/share/doc/libyaml-perl/copyright
/usr/share/doc/libyaml-perl/COMPATIBILITY
/usr/share/doc/libyaml-perl/changelog.gz
/usr/share/doc/libyaml-perl/changelog.Debian.gz
/usr/bin
/usr/bin/ysh
[isbear:~] cat dmp.pl
#! /usr/bin/perl

use YAML;
$YAML::DumpCode = 1;

sub a {
        print "Hello, World! I am born!\n";
        my $dump = Dump ( \&a );
        print "It's me:\n$dump\n";
}

a();

# The End.
[isbear:~] ./dmp.pl
Hello, World! I am born!
It's me:
--- !!perl/code |
{
    print "Hello, World! I am born!\n";
    my $dump = Dump(\&a);
    print "It's me:\n$dump\n";
}

[isbear:~]

Як бачите, тут жодної сторонньої бібліотеки - самі перлини...

[raven]

Як бачите, тут жодної сторонньої бібліотеки - самі перлини...

Ну...


[1]> ((lambda (arg)
   (list arg
         (list (quote quote)
               arg)))
 (quote (lambda (arg)
          (list arg
                (list (quote quote)
                      arg)))))
((LAMBDA (ARG) (LIST ARG (LIST 'QUOTE ARG)))
 '(LAMBDA (ARG) (LIST ARG (LIST 'QUOTE ARG))))
[2]>


Пекельно класичний приклад. В гуглі за першим лінком по даному запиту, до речі=)

[Михайло Даниленко]

Стало цікаво, як воно працює - докопався до оцього:
[isbear:~] cat dmp.pl
#! /usr/bin/perl

use B::Deparse;

sub a {
        print "Hello, World! I am born!\n";
        my $name = ( caller  0 ) [3];
        my $parser = B::Deparse->new ();
        my $me = $parser->deparse_sub ( B::svref_2object ( \&$name ) );
        print "Is it me? o_O\n$me\n";
}

a();

# The End.
[isbear:~] ./dmp.pl
Hello, World! I am born!
Is it me? o_O
{
        print "Hello, World! I am born!\n";
my $name = (caller 0)[3];
my $parser = 'B::Deparse'->new;
my $me = $parser->deparse_sub(B::svref_2object(\&$name));
print "Is it me? o_O\n$me\n";
}

B::svref_2object - це вже бінарна функція із стандартної бібліотеки

[Михайло Даниленко]

Ну... =)

[isbear:~] perl -e '&{sub { print qq{\&{$_[0]}(q{$_[0]})}}}(q{sub { print qq{\&{$_[0]}(q{$_[0]})}}})'
&{sub { print qq{\&{$_[0]}(q{$_[0]})}}}(q{sub { print qq{\&{$_[0]}(q{$_[0]})}}})[isbear:~]

[noddeat]

[Насправді, мене цікавить більш загальна ситуація: чи може функція бути власним значенням. Але оскільки тут не математики зібралися...]

я не те щоб математик, але що таке «власне значення функції»? може, мається на увазі оператор, а не функція?

[raven]

Ну... =)

[isbear:~] perl -e '&{sub { print qq{\&{$_[0]}(q{$_[0]})}}}(q{sub { print qq{\&{$_[0]}(q{$_[0]})}}})'
&{sub { print qq{\&{$_[0]}(q{$_[0]})}}}(q{sub { print qq{\&{$_[0]}(q{$_[0]})}}})[isbear:~]

Ну да, перл рулить=)

я не те щоб математик, але що таке «власне значення функції»? може, мається на увазі оператор, а не функція?

Мені здалося, що топікстартер силиться описати лямбду.

[Campana]

Так піде?

Пекельно класичний приклад. В гуглі за першим лінком по даному запиту, до речі=)

Тобто, якщо я створю файл із запропонованим вмістом, зроблю його виконуваним і запущу в консолі, то я отримаю сам вміст файлу на вивід, і все? Мене цікавить саме це.

я не те щоб математик, але що таке «власне значення функції»? може, мається на увазі оператор, а не функція?

Мені здалося, що топікстартер силиться описати лямбду.

Ага, точно. Я мав на увазі не власне значення оператора, а просто значення функції. Чи може значенням функції стати сама ця функція? Описово це саме λ, але це нічого не прояснює, бо
1) там немає засобів зробити функцію значенням самої себе. Все що там досягається, це позначення функції самої по собі.
2) λ-числення суперечливе. Тобто як теорія не годиться. Я, в принципі, знайшов чому: аксіома β не є коректною, бо її ліва частина не є такою. Колись я це опублікую.

[raven]

Тобто, якщо я створю файл із запропонованим вмістом, зроблю його виконуваним і запущу в консолі, то я отримаю сам вміст файлу на вивід, і все? Мене цікавить саме це.

Такий фінт вухами можна зробити і без особливих хитрощів. тинц-1, тинц-2.

Перший приклад на C убив і розірвав труп.

1) там немає засобів зробити функцію значенням самої себе. Все що там досягається, це позначення функції самої по собі.

λx.x ? Мгм... висловлюйтесь ясніше, я не телепат.

2) λ-числення суперечливе. Тобто як теорія не годиться. Я, в принципі, знайшов чому: аксіома β не є коректною, бо її ліва частина не є такою.

Шановний, ви про що? По-перше, вираз "некоректна аксіома" - явний оксюморон. По-друге, lambda це не теорія, а формалізм. По-третє, ткніть мене носом у протиріччя.

[Campana]

Тобто, якщо я створю файл із запропонованим вмістом, зроблю його виконуваним і запущу в консолі, то я отримаю сам вміст файлу на вивід, і все? Мене цікавить саме це.

Такий фінт вухами можна зробити і без особливих хитрощів. тинц-1,

О, здорово, дякую. Це вичерпна відповідь.

1) там немає засобів зробити функцію значенням самої себе. Все що там досягається, це позначення функції самої по собі.

λx.x ? Мгм... висловлюйтесь ясніше, я не телепат.

Та куди ж ясніше? А λx.x — це банальна функція y=x, вона тут ні до чого.

2) λ-числення суперечливе. Тобто як теорія не годиться. Я, в принципі, знайшов чому: аксіома β не є коректною, бо її ліва частина не є такою.

Шановний, ви про що? По-перше, вираз "некоректна аксіома" - явний оксюморон. По-друге, lambda це не теорія, а формалізм. По-третє, ткніть мене носом у протиріччя.

1) Це Ви просто незнайомі з проблематикою основ математики. Дуже грубий приклад: якщо аксіома передбачатиме маніпуляції із сумою розбіжного ряду, то вона буде некоректною.

2) Формалізми — це різновид теорій, а саме, це теорії виводу.

3) Ну, взагалі-то, це класика. Суперечливість λ-числення довів Клейні в тому ж чи в наступному році, як воно було оприлюднене. Чорч тоді закинув лямбду в запічок і більше ніколи нею не займався.

Доведення просте, як валянок, і використовує тільки аксіому β. На жаль, я його не пам'ятаю, але воно є в книзі Барендрегта.

Каррі намагався порятувати λ-числення своїми комбінаторами, але природу, зокрема логіку, не обдуриш: всі комбінаторні системи настільки слабкі, що не здатні моделювати вивід; якщо ж їх посилити (здається, достатньо додати modus ponens), вони стають суперечливими, як і довів Клейні.

[raven]

Та куди ж ясніше? А λx.x — це банальна функція y=x, вона тут ні до чого.

Ну, нехай. Просто я не бачу великої різниці між функцією і function pointer dereference.

1) Це Ви просто незнайомі з проблематикою основ математики. Дуже грубий приклад: якщо аксіома передбачатиме маніпуляції із сумою розбіжного ряду, то вона буде некоректною.

2) Формалізми — це різновид теорій, а саме, це теорії виводу.

3) Ну, взагалі-то, це класика. Суперечливість λ-числення довів Клейні в тому ж чи в наступному році, як воно було оприлюднене. Чорч тоді закинув лямбду в запічок і більше ніколи нею не займався.

Доведення просте, як валянок, і використовує тільки аксіому β. На жаль, я його не пам'ятаю, але воно є в книзі Барендрегта.

Каррі намагався порятувати λ-числення своїми комбінаторами, але природу, зокрема логіку, не обдуриш: всі комбінаторні системи настільки слабкі, що не здатні моделювати вивід; якщо ж їх посилити (здається, достатньо додати modus ponens), вони стають суперечливими, як і довів Клейні.

Я справді з подібними проблемами не знайомий. Дякую за наводки, почитаю. Але як тоді бути з Тьюрінг-повнотою лямбда-числення? λ - це класичний приклад Тьюрінг-повної системи, і, крім того, lisp just works.

[Campana]

Але як тоді бути з Тьюрінг-повнотою лямбда-числення? λ - це класичний приклад Тьюрінг-повної системи, і, крім того, lisp just works.

Ну так і теорія множин just works, хоча в ній всередині і парадокс Рассела, і парадокс Кантора, і парадокс Буралі-Форті і ще купа багів. Те, що суперечлива система буде повною в усіх смислах, зовсім не дивно: на те вона й суперечлива, що в ній все можна вивести.

Точніше сказати не можу, бо з алгоритмікою знайомий поки погано, все на логічному синтаксисі та семантиці пасуся. Однак, коректна перебудова λ-числення у мене на думці є: там треба тільки замінити λ-терми на зв'язані функційні змінні; логіка стане тим самим другопорядковою, дедуктивно неповною і нерозв'язною, зате суперечність має зникнути. Але перевірити це руки не доходять.