1

我正在为明天的最后一个练习表工作，我有点困惑，试图弄清楚问题在问什么以及如何解决它。我想在这里查一下，看看堆栈溢出的好人是否可以帮助我解决它。

问题是这样设置的：

显示一个派生树（它是类型检查的痕迹），证明以下表达式具有 type ：

(appC  (lamC ‘x   ???  (plusC (idC ‘x) (numC 1)))
  (numC 2) )

它基于这种类型检查的定义：

(define (typecheck [a : ExprC] [tenv : TypeEnv])
  (type-case ExprC a
  [numC (n) (numT)]
[plusC (l r) (typecheck-nums l r tenv)]
[multC (l r) (typecheck-nums l r tenv)]
[idC (n) (type-lookup n tenv)]
[lamC (n arg-type body)
      (arrowT arg-type
              (typecheck body 
                         (extend-env (tbind n arg-type)
                                     tenv)))]
[appC (fun arg)
      (type-case Type (typecheck fun tenv)
        [arrowT (arg-type result-type)
                (if (equal? arg-type
                            (typecheck arg tenv))
                    result-type
                    (type-error arg
                                (to-string arg-type)))]
        [else (type-error fun "function")])]))

(define (typecheck-nums l r tenv)
  (type-case Type (typecheck l tenv)
[numT ()
      (type-case Type (typecheck r tenv)
        [numT () (numT)]
        [else (type-error r "num")])]
[else (type-error l "num")]))

(define (type-error a msg)
(error 'typecheck (string-append
                 "no type: "
                 (string-append
                  (to-string a)
                  (string-append " not "
                                 msg)))))

当我在球拍中运行它时：

(typecheck (appC 
 (lamC 'x (numT) (plusC (idC 'x) (numC 1)))
 (numC 2))
mt-env)

我确实得到：

- Type
(numT)
- Type
(numT)

在底部它指出：

“您检查 'x 的类型必须是：numT”

所以它提出了 numT 但我对跟踪部分感到困惑，我知道这个问题很长，但这是所有练习问题中最让我困惑的一个。任何建议/帮助表示赞赏

4

1 回答 1

0

问题：“显示证明以下表达式具有类型的派生树”意味着您需要证明表达式具有给定类型。

考虑这个例子（与你的类型检查例子无关）：

评估表达式的结果(+ 1 2)具有类型int。为什么：

The subexpression 1 has type  int
The subexpression 2 has type  int
The subexpression + has type  int int -> int

由于上述类型，应用程序规则声明将 int int -> int 类型的函数应用于 int 类型的两个参数，具有 int 类型的结果。

类型检查器递归地检查表达式。它首先确定子表达式的类型，然后使用它们的类型来推断复合表达式的类型。

为了证明给定表达式具有某种类型，可以使用运行类型检查器的跟踪。要获取跟踪，请修改类型检查器以打印推断的类型。

未经测试的修改：

(define (typecheck [a : ExprC] [tenv : TypeEnv])
  (define (tell result-type)
    (display "The type of ")
    (display a)
    (display " is: ")
    (display result-type)
    (newline))

  (tell
   (type-case ExprC a
     [numC (n)               (numT)]
     [plusC (l r)            (typecheck-nums l r tenv)]
     [multC (l r)            (typecheck-nums l r tenv)]
     [idC (n)                (type-lookup n tenv)]
     [lamC (n arg-type body) (arrowT arg-type
                                     (typecheck body 
                                                (extend-env (tbind n arg-type)
                                                            tenv)))]
     [appC (fun arg)         (type-case Type (typecheck fun tenv)
                               [arrowT (arg-type result-type)
                                       (if (equal? arg-type
                                                   (typecheck arg tenv))
                                           result-type
                                           (type-error arg
                                                       (to-string arg-type)))]
                               [else (type-error fun "function")])])))
于 2015-05-07T06:59:46.427 回答