Попытка сделать основную программу на Haskell - PullRequest
0 голосов
/ 30 сентября 2019

Я пытаюсь создать некоторый код на Haskell, чтобы определить, является ли строка четной или нечетной.

even l evaluates to S 0 if l is a list of even length and evaluates to 0 if l is not of even length, for example

even a1:a2:a3:a4:#      --->   S 0    
even a1:a2:a3:a4:a5:#   --->   0    

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

execCBN :: Program -> Exp
execCBN (Prog e) = evalCBN e

evalCBN :: Exp -> Exp
evalCBN (EApp e1 e2) = case (evalCBN e1) of
    (EAbs i e1') -> evalCBN (subst i e2 e1')
    e1' -> EApp e1' e2
evalCBN (EIf e1 e2 e3 e4) = if (evalCBN e1) == (evalCBN e2) then evalCBN e3 else evalCBN e4
evalCBN (ELet i e1 e2) = evalCBN (EApp (EAbs i e2) e1) 
evalCBN (ERec i e1 e2) = evalCBN (EApp (EAbs i e2) (EFix (EAbs i e1)))
evalCBN (EFix e) = evalCBN (EApp e (EFix e)) 
evalCBN (EMinusOne e) = case (evalCBN e) of
    ENat0 -> ENat0
    (ENatS e) -> e
evalCBN (ENatS e') = ENatS (evalCBN e')
evalCBN x = x

1 Ответ

1 голос
/ 01 октября 2019

Во-первых, вот несколько советов по улучшению ваших будущих вопросов и ответов по 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))

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

...