Во-первых, вот несколько советов по улучшению ваших будущих вопросов и ответов по StackOverflow:
- Убедитесь, что ваш вопрос содержит Минимальный воспроизводимый пример . В вашем примере кода пропущены части, необходимые для запуска или даже понимания того, что происходит.
- Предоставьте достаточно контекста, чтобы сделать вопрос понятным: наличия в коде "CBN" было недостаточно, чтобы каждый комментатор понимал, чтопроисходило. Мне потребовалось некоторое усилие, чтобы понять, что вы имели в виду «внутри этого лямбда-вычислителя», и даже тогда «четная или нечетная строка» все еще не совсем очевидна: что такое строка? Вы хотите кодировать символьные строковые литералы, используя числа Пеано, или вы имеете в виду «является ли натуральное число с кодировкой Пеано четным или нечетным»?
- Если вы не предоставили достаточно контекстаВы очень затрудняете ответить на этот вопрос, потому что отвечающий должен будет либо приложить все усилия и воссоздать часть вашей ситуации, либо дать несколько ответов для каждой возможной интерпретации, либо сделать случайное предположение.
Во-вторых, вот моя интерпретация того, что вы спрашиваете:
Учитывая следующий интерпретатор лямбда-исчисления, как бы я создал Exp
, который представляет функцию, которая возвращает, еслизакодированное Пеано натуральное число является четным или нечетным? То есть, если мой even :: Exp
является EAbs "x" ...
, то
eval (EApp even zero) `shouldBe` true
eval (EApp even one) `shouldBe` false
eval (EApp even two) `shouldBe` true
eval (EApp even three) `shouldBe` false
eval (EApp even four) `shouldBe` true
where
zero = ENat0
one = ENatS zero
two = ENatS one
three = ENatS two
four = ENatS three
true = one
false = zero
Что бы вошло в even = EAbs "x" ...
?
И в-третьих, если бы я ответил, чтовопрос, я бы сказал:
Вы можете сделать это несколькими способами, но, поскольку у вашего лямбда-исчисления есть Fix
и Rec
, имело бы смысл попытаться выразить рекурсию через них. Вы могли бы начать с вопроса о том, как это делается в Haskell, затем абстрагировать рекурсию и затем преобразовать ее в интерпретатор лямбда-исчисления.
При таком подходе вы можете получить:
even :: Int -> Int
even 0 = 1
even 1 = 0
even n = even (n - 2)
Абстрагируясь от рекурсии , вы можете получить:
even :: Int -> Int
even = fix (\rec n ->
if n == 0 then 1 else
if n == 1 then 0 else
rec (n - 2))
Остальное я оставлю вам, чтобы вы могли использовать термины из вашего синтаксического дерева.