如何使用 haskell 添加函数和过程抽象指称语义？

Question

我想编写一个 haskell 程序来实现一种基于指称语义的简单命令式语言。我在 windows 上使用 GHCi，版本 8.4.2。我在实现下面描述的函数和过程抽象时遇到了一些问题。

让我描述一下。我称之为小鬼。首先，我定义了抽象语法。 IMP 只接受整数。标识符将是字符串。

    type      Numeral  = Int      
    type      Ident    = String

    data Command =
                  Skip
                | Assign   (Ident,       Expression)
                | Letin    (Declaration, Command   )
                | Cmdcmd   (Command,     Command   )
                | Ifthen   (Expression,  Command, Command)
                | Whiledo  (Expression,  Command   )
                | IdentifierC ( ActualParameter )

    data Expression =
                Num    Numeral
                | False_
                | True_
                | Notexp   Expression
                | Id       Ident
                | Sumof   (Expression,  Expression)
                | Subof   (Expression,  Expression)
                | Prodof  (Expression,  Expression)
                | Less    (Expression,  Expression)
                | Leten   (Declaration, Expression)
                | IdentifierE ( ActualParameter )
                  deriving Show

    type ActualParameter = Expression

    data FormalParameter = Constfp Identifier

    data Declaration =
              Constdef (Ident,  Expression)
            | Vardef   (Ident,  TypeDef   )
            | Func Identifier ( FormalParameter ) ~ Expression
            | Proce Identifier ( FormalParameter ) ~ Command
              deriving Show

    data TypeDef =
              Bool | Int
              deriving Show

简要说明：在 Command 中，Skip 什么都不做。 Assign 会将 Expression 的值赋给 Ident。 Letin 会在命令中声明一些变量。 Cmdcmd 会依次运行 2 个命令。 Ifthen 是条件命令，如果第一个表达式的计算结果为真，则运行第一个命令，否则第二个命令。 Whiledo 是循环。 IdentifierC ( ActualParameter ): IdentifierC 表示本地环境中的一些函数。这个 ActualParameter 是一些具有某些值的表达式。此命令仅在指定值上调用此函数。

表达式中，从上到下分别是：数字布尔假布尔真表达式的否定从本地环境中获取 Ident 的值。求和 2 个表达式减去 2 个表达式 2的产品 < 在表达式中声明一些变量 IdentifierE ( ActualParameter ) IdentifierE 表示本地环境中的某个函数。这个 ActualParameter 是一些具有某些值的表达式。此命令仅在指定值上调用此函数。这个表达式的结果终于得到了一个新值。

然后是语义域

    type    Integer = Int
    type    Boolean = Bool
    type    Location  = Int
    type    Function = Argument -> Store -> Value
    type    Procedure = Argument -> Store -> Store
    -- store would be snapshot of the memory.

    data    Value   = IntValue    Int
                    | TruthValue  Bool
                      deriving (Eq, Show)
    -- first class value only are int and bool

    type    Storable  = Value

    data    Bindable  = Const Value 
                      | Variable Location 
                      | Function Func 
                      | Procedure Proce
                      deriving (Eq, Show)

    data    Denotable = Unbound | Bound Bindable
                      deriving (Eq, Show)

    type    Argument = Value

    data Sval  = Stored Storable | Undef | Unused

    -- The actual storage in a Store
    type DataStore = Location -> Sval

    --                   --bot---   --top---  --data---
    data Store = Store (Location,  Location,  DataStore)

    type  Environ  =  Ident -> Denotable

    -- ---------- Semantic Functions -------------- --
    valuation :: Int         -> Value
    evaluate  :: Expression  -> Environ -> Store ->  Value
    elaborate :: Declaration -> Environ -> Store ->  (Environ,Store)
    execute   :: Command     -> Environ -> Store ->  Store

    -- the main goal is to define these semantic functions
    -- I give some examples in my source code below.

我的代码在这里：https://github.com/sanyuwen/IMP/blob/master/DSemImp.hs。我的测试代码在这里：https://github.com/sanyuwen/IMP/blob/master/ImpTest.hs

我在使用GHC导入DSemImp模块时，遇到了很多错误。

DSemImp.hs:52:32: error:
    Not in scope: type constructor or class ‘Identifier’
   |
52 | data FormalParameter = Constfp Identifier    |                                ^^^^^^^^^^
It said data FormalParameter = Constfp Identifier is not legal.
without this how can I define formal parameter ??

Answer 1

您没有定义 Identifier。虽然你定义了 Ident，但你是这个意思吗？

如何使用 haskell 添加函数和过程抽象指称语义？

How to add function and procedure abstractions denotational semantics using haskell?

haskell

denotational-semantics