对象式逻辑程序设计语言LKO的说明性语义

本文基于逻辑程序设计语言的良基模型语义，探讨了对象逻辑程序设计语言ＬＫＯ的说明性语义，该语义由组合迭代的极小不动点定义，具有构造性和组合性，迷在ＬＫＯ中进一步引入非单调继承和逻辑奠定了基础。     

一种基于ADT的函数语言及其操作语义模型

本文介绍一以ＡＤＴ为主要构件的函数语言，它是作者设计的函数式及面向对象式合成语言的函数部分，进而描述了其操作语义模型：多态λ演算十代数重写系统＝多态λ重写系统，并讨论该模型的Ｃｈｕｒｃｈ－Ｒｏｓｓｅｒ性质和强范式性质。     

逻辑程序的语义问题 I

文明性语义是逻辑程序研究的重要内容，也是其作为说明性程序的基本特征。近年来由于人们对带否定前提了一般逻辑程序设计的关注，以及逻辑程序与非单调推理的结合，逻辑程序的语义研究出现了许多新结果。本文以早期的Ｃｌａｒｋ语义和最小模型语义为起点，介绍这些新发展的部分内容，主要包括Ｃｌａｒｋ语义的Ｆｉｔｔｉｎｇ３－值扩充，理想模型语义，稳定模型语义，良基模型语义以及它们之间的关系，并在此基础上进一步讨论了说明     

LISP—ELP的设计和应用

1.引言 在本文中描述了LISP-ELP的特性、实现和应用。LISP-ELP是作者设计的一种支持专家系统程序设计的逻辑程序设计语言,它继承了LISP和Prolog两者的优点,改进了Prolog的控制结构,并具有极强的知识表达能力,该语言已经在IBM-PC微机上用C语言实现。 在“函数+逻辑”型语盲的研究中有[1,2]的工作.为了推进“函数+逻辑”型语言走向     

逻辑语言剪枝算子的过程语义及其实现

论述了逻辑程序设计中剪枝算子的作用及传统剪枝算子的过程性语义和说明性语义不一致问题;介绍了新型逻辑程序语言〔淑划中的COTRTT11t剪枝算子;通过引入一组定义描述其过程语义,并进一步阐述了剪枝算子和延迟计算规则之间的关系,讨论了Godel语言的剪枝策略及控制机制,从而为逻辑程序语言的实现提供了依据。     

动态模糊逻辑程序设计语言的指称语义

文献[8]借鉴Dijkstra的监督命令程序结构,给出了动态模糊逻辑程序设计语言的基本框架结构.在此基础上,进一步扩充和完善,并根据指称语义的原理和方法,用结构归纳法给出动态模糊逻辑程序设计语言的指称语义,主要包括:动态模糊程序设计语言的语义域、语义函数及其指称语义.最后给出了一个动态模糊程序设计语言的例子以观察程序的运行过程.     

合成语言FOPL基于方程逻辑的语义

程序设计语言ＦＯＰＬ是一种同时支持函数式程序设计风洛和面向对象程序设计风格的合成语言．本义介绍了ＦＯＰＬ的类型思想，并讨论了表达式纯洁性判断规则、表达式附类型规则及表达式等价判断规则，这些规则描述了ＦＯＰＬ基于方程逻辑的语义．     

G(o)del语言类型系统

G(o)del语言是一种说明性逻辑程序设计语言.该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义.详细介绍了G(o)del语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论.     

并发约束程序设计语言COPS及其执行模型

约束程序设计尤其是约束逻辑程序设计与并发约束程序设计在AI程序设计领域占据着越来越重要的位置。传统逻辑程序设计的基“计算即为定理证明”的计算风格虽获得了简洁优美的操作语义特性,但也付出了执行效率低的代价,当应用系统规模增大时,其性能严重下降以致崩溃。针对传统逻辑程序设计的这种可伸缩性问题,设计了一个基于并发约束程序设计概念的说明性语言COPS,旨在从语言设计与执行模型两方面降低说明性程序的不确定性,提高搜索与运行效率。在语言设计方面,通过引入确定性语言成分,避免不确定计算用于确定性目标所浪费的系统开销;在执行模型方面,在目标的并发穿叉执行与数据驱动的并发同步机制的基础上,实现“优先执行确定目标”策略与“最少假定”策略,作为约束传播的延伸,最大幅度地剪枝搜索空间,降低搜索复杂性。COPS提供的知识表示、推理与并发机制使其成为构造agent程序的理想语言。论文给出COPS语言的语法规范与执行模型的操作语义描述。     

Gödel语言类型系统

G(o)del语言是一种说明性逻辑程序设计语言.该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义.详细介绍了G(o)del语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论.     

A residualizing semantics for the partial evaluation of functional logic programs

Recent proposals for multi-paradigm declarative programming combine the most important features of functional, logic and concurrent programming into a single framework. The operational semantics of these languages is usually based on a combination of narrowing and residuation. In this paper, we introduce a non-standard, residualizing semantics for multi-paradigm declarative programs and prove its equivalence with a standard operational semantics. Our residualizing semantics is particularly relevant within the area of program transformation where it is useful, e.g., to perform computations during partial evaluation. Thus, the proof of equivalence is a crucial result to demonstrate the correctness of (existing) partial evaluation schemes.     

Towards the uniform implementation of declarative languages

Current implementation techniques for functional languages differ considerably from those for logic languages. This complicates the development of flexible and efficient abstract machines that can be used for the compilation of declarative languages combining concepts of functional and logic programming. We propose an abstract machine, called the JUMP-machine, which systematically integrates the operational concepts needed to implement the functional and logic programming paradigm. The use of a tagless representation for heap objects, which originates from the Spineless Tagless G-machine, supports the integration of different concepts. In this paper, we provide a functional logic kernel language and show how to translate it into the abstract machine language of the JUMP-machine. Furthermore, we define the operational semantics of the machine language formally and discuss the mapping of the abstract machine to concrete machine architectures. We tested the approach by writing a compiler for the functional logic language GTML. The obtained performance results indicate that the proposed method allows to implement functional logic languages efficiently.     

The narrowing-driven approach to functional logic program specialization

Partial evaluation is a semantics-based program optimization technique which has been investigated within different programming paradigms and applied to a wide variety of languages. Recently, a partial evaluation framework for functional logic programs has been proposed. In this framework, narrowing—the standard operational semantics of integrated languages—is used to drive the partial evaluation process. This paper surveys the essentials of narrowing-driven partial evaluation. Elvira Albert, Ph.D.: She is an associate professor in Computer Science at the Technical University of Valencia, Spain. She received her bachelors degree in computer science in 1998 and her Ph.D. in computer science in 2001, both from the Technical University of Valencia. She has investigated on program optimization and on partial evaluation for declarative multi-paradigm programming languages. Her current research interests include term rewriting, multi-paradigm declarative programming, and formal methods, in particular semantics-based program analysis, transformation, specification, verification, and debugging. Germán Vidal, Ph.D.: He is an associate professor in Computer Science at the Technical University of Valencia, Spain. He obtained his bachelors degree in computer science in 1992 and his Ph.D. in computer science in 1996, both from the Technical University of Valencia. He is active on several research topics in Functional Logic Programming. He has worked on compositionality, on abstract interpretation, and on program transformation techniques for functional logic programs. Currently, his research interests include declarative multi-paradigm programming languages, term rewriting, and semantics-based program manipulation, in particular partial evaluation.     

Effective incorporation of function into logic

During the last decade, the integration of functional and logic languages has received widespread attraction for the purpose of offering two different programming styles in one system simultaneously. The main goal is to incorporate the characteristics of the two paradigms coherently, without degrading the performance of the whole system. However, few languages have achieved this goal. Some of them, even though they have a rich set of functions, perform poorly. Others are efficient, but lose some important facilities. The paper proposes a functional logic language Lazy Aflog and its abstract machine FWAM-II as an expressive and efficient mechanism for this incorporation. Lazy Aflog is an extension of logic language in which functions are reduced in the extended unification, called E-unification with lazy evaluation. This extended unification allows Lazy Aflog to process infinite data structures and higher-order functions naturally. FWAM-II is an extension of the Warren Abstract Machine (WAM) in which the instructions and run-time structures to provide the suspension/reactivation of functional closure are added. These facilities enable FWAM-II to support not only resolution but also infinite data structures and higher-order functions efficiently. In addition, the experimental results show that Lazy Aflog and FWAM-II could be a good compromise between expressiveness and efficiency of the integration.     

函数式语言并行实现中并行颗粒度的动态控制

本文针对并行处理中并行颗粒度的控制问题，将惰性计值的延迟思想引入并行进程的生成过程中，并与文献［１，２］的ＬＥ计值语义相结合，提出了函数式语言的并行ＬＥ计值语义，由于采用ＩＨＲＥＡＤ来实现对并行归约子进程的延迟处理，使得并行计算进程在运行时可以动态增加其并行颗粒度，从而减少了一些不必要的细粒度并行性的开发，与文献［５］相比，由于基于负载的动态内联思想在延迟处理操作中的引入亦进一步减少了很大一部分延     

Formulae Meet Programs Over the Net: A Framework for Correct Network Aware Programming

A general framework for network aware programming is presented that consists of a language for programming mobile applications, a logic for specifying properties of the applications and an automatic tool for verifying such properties. The framework is based on X-KLAIM, eXtended KLAIM, an experimental programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code. The proposed logic is a modal logic inspired by Hennessy-Milner logic and is interpreted over the same labelled structures used for the operational semantics of X-KLAIM. The automatic verification tool is based on a complete proof system that has been previously developed for the logic.     

A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.     

On a decision procedure for quantified linear programs

Quantified linear programming is the problem of checking whether a polyhedron specified by a linear system of inequalities is non-empty, with respect to a specified quantifier string. Quantified linear programming subsumes traditional linear programming, since in traditional linear programming, all the program variables are existentially quantified (implicitly), whereas, in quantified linear programming, a program variable may be existentially quantified or universally quantified over a continuous range. In this paper, the term linear programming is used to describe the problem of checking whether a system of linear inequalities has a feasible solution. On account of the alternation of quantifiers in the specification of a quantified linear program (QLP), this problem is non-trivial. QLPs represent a class of declarative constraint logic programs (CLPs) that are extremely rich in their expressive power. The complexity of quantified linear programming for arbitrary constraint matrices is unknown. In this paper, we show that polynomial time decision procedures exist for the case in which the constraint matrix satisfies certain structural properties. We also provide a taxonomy of quantified linear programs, based on the structure of the quantifier string and discuss the computational complexities of the constituent classes. This research has been supported in part by the Air Force Office of Scientific Research under contract FA9550-06-1-0050.