A pattern, i.e., a term possibly with variables, denotes the set
(language) of all its ground instances. In an untyped setting,
symbolic operations on finite sets of patterns can represent Boolean
operations on languages. But for the more expressive patterns needed
in declarative languages supporting rich type disciplines such as
subtype polymorphism untyped pattern operations and algorithms break
down. We show how they can be properly defined by means of a
signature transformation that enriches the types of the original
signature. We also show that this transformation allows a systematic
reduction of the first-order logic properties of an initial
order-sorted algebra supporting subtype-polymorphic functions to
equivalent properties of an initial many-sorted (i.e., simply typed)
algebra. This yields a new, simple proof of the known decidability of
the first-order theory of an initial order-sorted algebra.
This is the default collection for all research and scholarship developed by faculty, staff, or students at the University of Illinois at Urbana-Champaign
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
