Как только решение было найдено в лямбда-исчислении, насколько легко преобразовать его в код?

Если бы вы прочитали условие задачи, такое как что-то найденное на TopCoder, и преобразовали его в представление лямбда-исчисления, было бы простым упражнением «преобразовать» его в код Haskell или Lisp?

Другими словами, можно ли решить проблему, используя формальную систему лямбда-исчисления, а затем тривиально реализовать на функциональном языке программирования?


functional-programming haskell lisp lambda-calculus
person Daniel Levin    schedule 18.04.2012    source источник
comment
Я считаю (но не могу/не докажу), что было бы тривиально перевести любую программу, написанную на просто типизированном лямбда-исчислении, на Haskell (есть функции, которые вы можете написать на нетипизированном лямбда-исчислении, которые вы не можете написать на Haskell). ). Glasgow Haskell преобразует сахар в SystemF, который, грубо говоря, является более мощной версией простого типизированного лямбда-исчисления, поэтому Haskell уже включает STLC. Ваш перевод просто должен быть преобразован в крошечное подмножество Haskell, которое не содержит сахара - естественно, результат будет очень подробным и неидиоматичным.   -  person stephen tetley    schedule 18.04.2012
comment
@stephentetley: На самом деле нечего доказывать. Перевод очень тривиальный, λx:τ. M переводится в \(x :: τ) -> M, а приложение функции M N остается прежним. Проблема возникает с нетипизированным лямбда-исчислением, поскольку есть термы, которые нельзя типизировать без свертывания/развертывания бесконечных типов (очень хороший пример — комбинатор Y).   -  person Vitus    schedule 18.04.2012

Ответы (2)


arrow_upward
3
arrow_downward

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

Из любопытства, кто черт возьми решает TopCoder с помощью лямбда-исчисления? Это звучит весьма нетривиально. о_О

person MathematicalOrchid    schedule 18.04.2012
comment
так что в этом смысле Lisp может быть проще для перевода, потому что он также нетипизирован? - person newacct; 18.04.2012
comment
Во сне у меня возникают высокоуровневые (бессознательные) мысли. Моя кошка разбудила меня в 3 часа ночи, и это то, что просочилось в мое сознание. Я услышал вопрос в своей голове и начал рассматривать использование лямбда-исчисления в качестве промежуточного представления проблемы. Я бы сделал это, потому что это позволило бы преобразовать многословную постановку задачи во что-то чисто символическое. Результатом этого в идеале должна быть простая, урезанная до костей вычислительная задача, а не высокоуровневое описание. По сути, целью является сведение «реальной» системы к математической/вычислительной. - person Daniel Levin; 18.04.2012
comment
(λnmfx. n(mf)x)(λfx. f(fx))(λfx. f(fx)) — это очень, действительно многословный способ сказать 2 + 2. ;-) - person MathematicalOrchid; 04.06.2012

arrow_upward
0
arrow_downward

Это сложный вопрос. Теоретически да. На практике вроде. В общем, я бы сказал, что определенные вычислимые функции могут быть эффективно реализованы (во временном пространстве усилий программиста), да, но это действительно зависит от знакомства с языком программирования и рассматриваемой математики, а не возможность сделать это . Например, я полагаю, что можно было бы реализовать интерпретатор лямбда-исчисления, и я отсылаю вас к ['Visual Automata Simulator]'1 для примера модели Тьюринга, содержащейся в упрощенной оболочке.

person jcc333    schedule 18.04.2012
comment
Я полагаю, что можно было бы реализовать интерпретатор лямбда-исчисления - да, довольно легко. Нетипизированное лямбда-исчисление является первым в серии все более сложных языков, представленных в разделе Типы и языки программирования. Реализации в OCaml: cis.upenn.edu/~bcpierce/tapl - person Dan Burton; 18.04.2012
comment
Введение к этой книге: Система типов — это синтаксический метод обеспечения уровней абстракции в программах. ПОТЕРПЕТЬ ПОРАЖЕНИЕ! - person Kaz; 18.04.2012