A MATCHING PROCEDURE FOR W-ORDER LOGIC

Abstract

Formation rules are presented for an W-order logic with lambda operator in which each term has a well defined type. Transformation rules are given defining lambda-conversion, special conversion, substitution, and alphabetic change of bound variables. The notion of one term being an 'instance' of another is then defined using these transformation rules. The main problem of the paper is to develop a 'matching procedure' for pairs of terms, so that every common instance of the two given terms is an instance of some term produced by the matching procedure. This is accomplished by analysing the terms according to the formation rules, matching the outermost parts first, then proceeding inductively inward. Examples are given to show that an infinite set of terms may be needed for this purpose. Conditions under which such an infinite set is needed are discussed. A procedure is developed for producing at least one common instance, if one exists.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 15, 1966
Accession Number
AD0646560

Entities

People

  • William E. Gould

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Classification
  • Continents
  • Contracts
  • Conversion
  • Corporations
  • Department Of Defense
  • Elimination
  • Geographic Regions
  • Mathematics
  • New Jersey
  • Security
  • Standards
  • United States
  • Universities

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design