Haskell lambda表达式和简单的逻辑公式

1 回答

• 10

  这是一个像游戏一样使用Agda _785179的好时机 . 你也可以手动完成它，但是我做了什么：

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = ?
  
  Goal: B
  x : (((A -> B) -> A) -> A) -> B
  

  基本上我们唯一的举动是申请 x ，所以让我们试试吧 .

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = x ?
  
  Goal: ((A -> B) -> A) -> A 
  x : (((A -> B) -> A) -> A) -> B
  

  现在我们的目标是一个函数类型，所以让我们尝试一个lambda .

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = x (\y -> ?)
  
  Goal: A 
  x : (((A -> B) -> A) -> A) -> B
  y : (A -> B) -> A
  

  我们需要一个 A ，如果我们提供正确的参数， y 可以给我们 . 不确定那是什么，但 y 是我们最好的选择：

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = x (\y -> y ?)
  
  Goal: A -> B
  x : (((A -> B) -> A) -> A) -> B
  y : (A -> B) -> A
  

  我们的目标是函数类型，所以让我们使用lambda .

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = x (\y -> y (\z -> ?))
  
  Goal: B
  x : (((A -> B) -> A) -> A) -> B
  y : (A -> B) -> A
  z : A
  

  现在我们需要 B ，唯一可以给我们 B 的东西是 x ，所以让我们再试一次 .

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = x (\y -> y (\z -> x ?))
  
  Goal: ((A -> B) -> A) -> A
  x : (((A -> B) -> A) -> A) -> B
  y : (A -> B) -> A
  z : A
  

  现在我们的目标是返回 A 的函数类型，但是我们有 z 这是 A 所以我们不要忽略它并返回 z .

  f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
  f x = x (\y -> y (\z -> x (\_ -> z)))
  

  你去吧！

  回复于 2024-04-28T14:45:33+08:00