типа объединения Isabelle/вывод ошибка

Question

Я только начал в Изабелле, и я получаю сообщение об ошибке объединения типа при работе через упражнения 3.3 в из Concrete Semantics:

Определит функцию замещения

subst :: vname ⇒ aexp ⇒ aexp ⇒ aexp 

такой, что subst x a e является результатом замены каждого вхождения переменной x на a в e. Например:

subst ''x'' (N 3) (Plus (V ''x'') (V ''y'')) = Plus (N 3) (V ''y'') 

Вот что у меня до сих пор:

theory Scratchpad 
imports Main 
begin 

type_synonym vname = string 
type_synonym val = int 
type_synonym state = "vname ⇒ val" 

datatype aexp = N int | V vname | Plus aexp aexp 

fun subst :: "vname ⇒ aexp ⇒ aexp ⇒ aexp" where 
"subst x (N a) (N e) = (N e)" | 
"subst x (N a) (V e) = (if x=e then (N a) else (V e))" | 
"subst x (N a) (Plus e1 e2) = Plus(subst(x (N a) e1) subst(x (N a) e2))" 

end 

Когда третий случай в определении функции закомментирован, выполнение тестов

value "subst ''x'' (N 3) (N 5)" 
value "subst ''x'' (N 3) (V ''x'')" 

производит (N 5) и (N 3) соответственно, поэтому я знаю, что первые две строки работают правильно. Суммируя последние результаты строки в сообщении об ошибке

Тип объединение потерпело неудачу: Clash типов «_ ⇒ _» и «_» список ошибок

Типа в применении: оператор не типа функции

оператора : х :: голец список
Операнд: N A :: Aexp

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

Что означают сообщения об ошибках (конкретно и вообще), и как это исправить?

Answer 1

Чтобы ответить на ваш вопрос о котировках: две одиночные кавычки используются в Isabelle/HOL (точнее его внутренний синтаксис) для обозначения строковых литералов. То есть, по ''abc'' мы обозначаем строку, содержащую три символа a, b и c (что снова использовало бы специальный синтаксис, если бы вам пришлось вводить их буквально). Двойные кавычки, с другой стороны, в основном используются для разделения операторов Isar (внешний синтаксис) из терминов внутри логики. Таким образом, хотя ''...'' является частью языка терминов, "..." нет.

Теперь для сообщения об ошибке. Он сообщает вам, что вы пытаетесь использовать список x (тип _ list) как функция (тип _ => _). Почему Изабель думает, что вы хотите использовать x в качестве функции? Хорошо, потому что сопоставление (то есть, запись терминов рядом друг с другом, разделенное пробелом) обозначает функциональное приложение.Таким образом, x (N a) интерпретируется как применение функции x к аргументу (N a) (точно так же, как f y - приложение f к аргументу y). Чтобы дать вашему определению правильное значение, вы должны использовать скобки в правильных положениях. Я предполагаю, что вы хотели в вашем третьем пункте было:

Plus (subst x (N a) e1) (subst x (N a) e2) 

, где мы имеем два вхождения функции subst применительно к трем аргументам. (Так что это был вопрос синтаксиса в конце концов;).

Другой комментарий. Ваша реализация subst может быть более общей. Как есть, второй аргумент subst всегда фиксируется как некоторое число a (из-за использования вами конструктора N). Однако все должно работать так же хорошо, если вы допустили произвольные выражения типа aexp.