Представление связанных переменных с помощью функции от использования к связующим

Проблема представления связанных переменных в синтаксисе и, в частности, проблема подстановки во избежание захвата, хорошо известна и имеет ряд решений: именованные переменные с альфа-эквивалентностью, индексы де Брейна, локальное безымянность, именные множества и т. Д.

Но, похоже, есть еще один довольно очевидный подход, который я, тем не менее, нигде не видел. А именно, в базовом синтаксисе у нас есть только один «переменный» термин, написанный, скажем, , а затем отдельно мы даем функцию, которая отображает каждую переменную в подшивку, в рамках которой она лежит. Так что λ- термин, как$\bullet$$\lambda$

будет написано , и функция отобразит первый ∙ на первый λ, а второй ∙ на второй λ . Так что это похоже на индексы де Брюйна, только вместо того, чтобы «считать λ s», когда вы выходите из термина, чтобы найти соответствующее связующее, вы просто оцениваете функцию. (Если представить это как структуру данных в реализации, я бы подумал о том, чтобы снабдить каждый объект с переменным членом простым указателем / ссылкой на соответствующий объект с связующим термином.)$\lambda. (\lambda. \bullet\bullet)$$\bullet$$\lambda$$\bullet$$\lambda$$\lambda$

Очевидно, что это не имеет смысла для написания синтаксиса на странице для чтения людьми, но в то же время это не индексы де Брейна. Мне кажется, что в математическом плане это имеет смысл, и, в частности, это делает замену без захвата очень простой: просто отбросьте термин, который вы заменяете, и возьмите объединение функций связывания. Это правда, что в нем нет понятия «свободная переменная», но (опять же), на самом деле, индексы де Брейна тоже не работают; в любом случае термин, содержащий свободные переменные, представляется термином со списком «контекстных» связывателей впереди.

Я что-то упустил, и по какой-то причине это представление не работает? Есть ли проблемы, которые делают его намного хуже, чем другие, о которых не стоит задумываться? (Единственная проблема, о которой я могу подумать сейчас, заключается в том, что набор терминов (вместе с их связывающими функциями) не определен индуктивно, но это не кажется непреодолимым.) Или действительно есть места, где он использовался?

Ответы Андрея и Лукаша дают хорошие результаты, но я хотел добавить дополнительные комментарии.

Чтобы повторить то, что сказал Дамиано, этот способ представления связывания с помощью указателей - это тот, который был предложен сетями доказательств, но самое раннее место, где я увидел это для лямбда-терминов, было в старом эссе Кнута:

• Дональд Кнут (1970). Примеры формальной семантики. В Симпозиуме по семантике алгоритмических языков , Э. Энгелер (ред.), Лекционные заметки по математике 188, Springer.

$(\lambda y.\lambda z.yz)x$

Этот вид графического представления лямбда-терминов также изучался независимо (и более глубоко) в двух тезисах в начале 1970-х годов, как Кристофером Уодсвортом (1971, Семантика и прагматика лямбда-исчисления ), так и Ричардом Стэтманом (1974, Структурная сложность). доказательств ). В настоящее время такие диаграммы часто называют «λ-графами» (см., Например, эту статью ).

Заметьте, что термин на диаграмме Кнута является линейным в том смысле, что каждая свободная или связанная переменная встречается ровно один раз - как уже упоминали другие, существуют нетривиальные проблемы и решения, которые необходимо сделать, пытаясь распространить такое представление на не -линейные условия.

$\alpha$

Я не уверен, как будет представлена ​​ваша функция-переменная-связка и для какой цели вы хотите ее использовать. Если вы используете обратные указатели, то, как заметил Андрей, вычислительная сложность замещения не лучше классического альфа-переименования.

Из вашего комментария к ответу Андрея я делаю вывод, что вы в некоторой степени заинтересованы в обмене. Я могу предоставить некоторую информацию здесь.

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

Давайте добавим некоторый синтаксис:

$C_a^{b,c}(\cdot)$$a$$b,c$

С этим синтаксисом каждая переменная используется ровно дважды, один раз, где она связана, и один раз, где она используется. Это позволяет нам дистанцироваться от определенного синтаксиса и рассматривать термин как график, где переменные и термины являются ребрами.

Из алгоритмической сложности теперь мы можем использовать указатели не от переменной к связующему, а от привязки к переменной и иметь замены в постоянном времени.

Кроме того, эта переформулировка позволяет нам отслеживать удаление, копирование и передачу с большей точностью. Можно написать правила, которые постепенно копируют (или стирают) термин, разделяя подтермы. Есть много способов сделать это. В некоторых ограниченных условиях выигрыши довольно удивительны .

Это становится ближе к темам сетей взаимодействия, комбинаторов взаимодействия, явного замещения, линейной логики, оптимальной оценки Лэмпинга, совместного использования графиков, логики освещения и других.

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

Ваша структура данных работает, но она не будет более эффективной, чем другие подходы, потому что вам нужно копировать каждый аргумент в каждом бета-сокращении, и вам нужно сделать столько копий, сколько вхождений связанной переменной. Таким образом, вы продолжаете разрушать разделение памяти между подтермами. В сочетании с тем фактом, что вы предлагаете не чистое решение, которое включает в себя манипуляции с указателями и, следовательно, очень подвержено ошибкам, оно, вероятно, не стоит проблем.

Но я был бы рад увидеть эксперимент! Вы можете взять lambdaи реализовать это с вашей структурой данных (в OCaml есть указатели, они называются ссылками ). Более или менее, вам просто нужно заменить syntax.mlи norm.mlвашими версиями. Это менее 150 строк кода.

Другие ответы в основном обсуждают вопросы реализации. Поскольку вы упоминаете свою основную мотивацию как выполнение математических доказательств без излишней бухгалтерии, вот основная проблема, которую я вижу в этом.

Когда вы говорите «функция, которая отображает каждую переменную в подшивку, в область действия которой она входит»: тип вывода этой функции, безусловно, немного более тонкий, чем это делает ее звучащей! В частности, функция должна принимать значения в чем-то вроде «связующих элементов рассматриваемого термина» - то есть некоторого набора, который варьируется в зависимости от термина (и, очевидно, не является подмножеством большего набора окружений каким-либо полезным способом). Таким образом, в подстановке вы не можете просто «взять объединение функций привязки»: вы также должны переиндексировать их значения в соответствии с некоторой картой от связывателей в исходных терминах до связывателей в результате подстановки.

Эти переиндексации, безусловно, должны быть «рутинными» в том смысле, что их можно было бы либо смести под ковер, либо красиво упаковать с точки зрения некоторой функториальности или естественности. Но то же самое относится и к бухгалтерии, связанной с работой с именованными переменными. В целом, мне кажется, что с этим подходом будет связано как минимум столько же бухгалтерии, сколько с более стандартными подходами.

Однако, кроме этого, это концептуально очень привлекательный подход, и я хотел бы, чтобы он был тщательно проработан - я могу себе представить, что он может пролить свет на некоторые аспекты синтаксиса, чем стандартные подходы.

$\lambda$Lazy.t

В целом, я думаю, что это классное представление, но оно включает в себя некоторую бухгалтерию с указателями, чтобы избежать разрыва обязательных ссылок. Я думаю, можно было бы изменить код для использования изменяемых полей, но тогда кодирование в Coq было бы менее прямым. Я все еще убежден, что это очень похоже на HOAS, хотя структура указателя сделана явной. Тем не менее, наличие Lazy.tподразумевает, что некоторый код может быть оценен в неправильное время. В моем коде дело обстоит иначе, так как во forceвремя может происходить только замена переменной на переменную (а не оценка, например).

(* Representation of a term of the λ-calculus. *)
type term =
  | FVar of string      (* Free variable  *)
  | BVar of bvar        (* Bound variable *)
  | Appl of term * term (* Application    *)
  | Abst of abst        (* Abstraction    *)

(* A bound variable is a pointer to the corresponding binder. *)
and bvar = abst

(* A binder is represented as its body in which the bound variable points to
   the binder itself. Note that we need to use a thunk to be able to work
   underneath a binder (for substitution, evaluation, ...). A name can be
   given for easy printing, but no renaming is done. Only “visual capture”
   can happen since pointers are established the right way, even if names
   can clash. *)
and abst = { body : term Lazy.t ; name : string }

(* Terms can be built with recursive values for abstractions. *)

(* Krivine's notation is used for application (function in parentheses). *)

let id    : term = (* λx.x        *)
  Abst(let rec id = {body = lazy (BVar(id)); name = "x"} in id)

let idid  : term = (* (λx.x) λx.x *)
  Appl(id, id)

let delta : term = (* λx.(x) x *)
  Abst(let rec d = {body = lazy (Appl(BVar(d), BVar(d))); name = "x" } in d)

let weird : term = (* (λx.x) λy.(λx.(x) x) (C) y *)
  Appl(id, Abst(let rec x = {body = lazy (Appl(delta, Appl(FVar("C"),
    BVar(x)))); name = "y"} in x))

let omega : term = (* (λx.(x) x) λx.(x) x *)
  Appl(delta, delta)

(* Printing function is immediate. *)
let rec print : out_channel -> term -> unit = fun oc t ->
  match t with
  | FVar(x)   -> output_string oc x
  | BVar(x)   -> output_string oc x.name
  | Appl(t,u) -> Printf.fprintf oc "(%a) %a" print t print u
  | Abst(f)   -> Printf.fprintf oc "λ%s.%a" f.name print (Lazy.force f.body)

(* Substitution of variable [x] by [v] in the term [t]. Occurences of [x] in
   [t] are identified using physical equality ([BVar] case). The subtle case
   is [Abst], because we need to reestablish the physical link between the
   binder and the variable it binds. *)
let rec subst_var : bvar -> term -> term -> term = fun x t v ->
  match t with
  | FVar(_)   -> t
  | BVar(y)   -> if y == x then v else t
  | Appl(t,u) -> Appl(subst_var x t v, subst_var x u v)
  | Abst(f)   ->
      (* First compute the new body. *)
      let fv = subst_var x (Lazy.force f.body) v in
      (* Reestablish the physical link, using [subst_var] itself again. This
         requires a second traversal of the term. We could probably do both
         at once, but who cares the complexity is linear in [t] anyway. *)
      Abst(let rec g = {f with body = lazy (subst_var f fv (BVar(g)))} in g)

(* Actual substitution function. *)
let subst : abst -> term -> term = fun f v ->
  subst_var f (Lazy.force f.body) v

(* Normalization function (all the way, even under binders). *)
let rec eval : term -> term = fun t ->
  match t with
  | Appl(t,u) ->
      begin
        let v = eval u in
        match eval t with
        | Abst(f) -> eval (subst f v)
        | t       -> Appl(t,v)
      end
  | Abst(f)   ->
      (* Actual computation in the body. *)
      let fv = eval (Lazy.force f.body) in
      (* Here, the physical link is reestablished, but it is important to note
         that the computation of evaluation is done above. So the part below
         only takes a linear time in the size of the normal form of the body
         of the abstraction. *)
      Abst(let rec g = {f with body = lazy (subst_var f fv (BVar(g)))} in g)
  | _         ->
      t

let _ = Printf.printf "id         = %a\n%!" print id
let _ = Printf.printf "eval id    = %a\n%!" print (eval id)

let _ = Printf.printf "idid       = %a\n%!" print idid
let _ = Printf.printf "eval idid  = %a\n%!" print (eval idid)

let _ = Printf.printf "delta      = %a\n%!" print delta
let _ = Printf.printf "eval delta = %a\n%!" print (eval delta)

let _ = Printf.printf "omega      = %a\n%!" print omega
(* The following obviously loops. *)
(*let _ = Printf.printf "eval omega = %a\n%!" print (eval omega)*)

let _ = Printf.printf "weird      = %a\n%!" print weird
let _ = Printf.printf "eval weird = %a\n%!" print (eval weird)

(* Output produced:
id         = λx.x
eval id    = λx.x
idid       = (λx.x) λx.x
eval idid  = λx.x
delta      = λx.(x) x
eval delta = λx.(x) x
omega      = (λx.(x) x) λx.(x) x
weird      = (λx.x) λy.(λx.(x) x) (C) y
eval weird = λy.((C) y) (C) y
*)