Что это значит, когда у вас есть несколько строк, определяющих действие индуктивного конструктора? - PullRequest
Новая
       7

Что это значит, когда у вас есть несколько строк, определяющих действие индуктивного конструктора?

0 голосов
/ 13 декабря 2018

Я смотрел на: 

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum  : forall (n: nat),
      aevalR (ANum n) n
  | E_APlus : forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus: forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult : forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (AMult e1 e2) (n1 * n2).

и пытался понять, что это значит.Я понимаю, что это требует арифметического опыта.отображает это на функцию, которая отображает на нат, который отображается на реквизит.Но что меня смущает, так это то, что находится внутри предложений | A_AOp.У них нет периода в конце, а у плюса и минуса есть стрелка, указывающая на другую стрелку.

Что это за синтаксис и что он говорит?Какой вклад в этот индуктивный тип?Как обычно я вижу в python: 

def f(a,b,*args):

, поэтому я знаю, что я должен дать в качестве входных данных (более или менее).Но этот смущает меня.Как мне это использовать и что означает определение?

idk, если это простой вопрос функционального программирования или нет, так как я только изучаю Coq и функциональное программирование, а эта часть не была в введении в функциональное программирование курса, на который я смотрел:

https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html

1 Ответ

0 голосов
/ 13 декабря 2018

Этот фрагмент определяет предикат aevalR индуктивно.Предикат является отношением между выражениями e : aexp и числами n : nat: aevalR e n сохраняется, когда e оценивается как n.Каждое предложение, представленное вертикальной чертой, описывает одну из возможностей оценки выражения.Например, E_APlus говорит, что когда e1 оценивается в n1, а e2 оценивается в n2, мы знаем, что APlus e1 e2 оценивается в n1 + n2.

Индуктивные суждения являются одним изнаиболее используемые инструменты в Coq.В книге «Основы программного обеспечения» есть глава , которая представляет эту концепцию.Я советую вам ознакомиться с этой концепцией, прежде чем пытаться атаковать главу о бесах - это должно значительно облегчить чтение.

...